Welcome!
>> Specification generalized.lf.
>> Schema c := {T}(x:tm,y:of x T).
>> Theorem subject_reduction:
ctx Gamma:c,
forall M1 M2 T D1 D2,
{Gamma |- D1 : step M1 M2} =>
{Gamma |- D2 : of M1 T} => exists D3, {Gamma |- D3 : of M2 T}.
Subgoal subject_reduction:
==================================
ctx Gamma:c,
forall M1, forall M2, forall T, forall D1, forall D2,
{Gamma |- D1 : step M1 M2} =>
{Gamma |- D2 : of M1 T} => exists D3, {Gamma |- D3 : of M2 T}
subject_reduction>> induction on 1.
Subgoal subject_reduction:
IH:
ctx Gamma:c,
forall M1, forall M2, forall T, forall D1, forall D2,
{Gamma |- D1 : step M1 M2}* =>
{Gamma |- D2 : of M1 T} => exists D3, {Gamma |- D3 : of M2 T}
==================================
ctx Gamma:c,
forall M1, forall M2, forall T, forall D1, forall D2,
{Gamma |- D1 : step M1 M2}@ =>
{Gamma |- D2 : of M1 T} => exists D3, {Gamma |- D3 : of M2 T}
subject_reduction>> intros.
Subgoal subject_reduction:
Vars: D2:o, D1:o, T:o, M2:o, M1:o
Contexts: Gamma{}:c[]
IH:
ctx Gamma:c,
forall M1, forall M2, forall T, forall D1, forall D2,
{Gamma |- D1 : step M1 M2}* =>
{Gamma |- D2 : of M1 T} => exists D3, {Gamma |- D3 : of M2 T}
H1:{Gamma |- D1 : step M1 M2}@
H2:{Gamma |- D2 : of M1 T}
==================================
exists D3, {Gamma |- D3 : of M2 T}
subject_reduction>> cases H1.
Subgoal subject_reduction.1:
Vars: D:(o) -> (o) -> o, R1:(o) -> o, T1:o, R2:(o) -> o, D2:o, T:o
Nominals: n3:o, n2:o, n1:o, n:o
Contexts: Gamma{n, n1, n2, n3}:c[]
IH:
ctx Gamma:c,
forall M1, forall M2, forall T, forall D1, forall D2,
{Gamma |- D1 : step M1 M2}* =>
{Gamma |- D2 : of M1 T} => exists D3, {Gamma |- D3 : of M2 T}
H2:{Gamma |- D2 : of (lam T1 ([c4]R1 c4)) T}
H3:{Gamma |- T1 : ty}*
H4:{Gamma, n:tm |- R1 n : tm}*
H5:{Gamma, n1:tm |- R2 n1 : tm}*
H6:{Gamma, n2:tm, n3:of n2 T1 |- D n2 n3 : step (R1 n2) (R2 n2)}*
==================================
exists D3, {Gamma |- D3 : of (lam T1 ([c55]R2 c55)) T}
Subgoal subject_reduction.2 is:
exists D3, {Gamma |- D3 : of (R N) T}
Subgoal subject_reduction.3 is:
exists D3, {Gamma |- D3 : of (app M N2) T}
Subgoal subject_reduction.4 is:
exists D3, {Gamma |- D3 : of (app M4 N) T}
subject_reduction.1>> cases H2.
Subgoal subject_reduction.1:
Vars: D3:(o) -> (o) -> o, T2:o, D:(o) -> (o) -> o, R1:(o) -> o, T1:o, R2:
(o) -> o
Nominals: n6:o, n5:o, n4:o, n3:o, n2:o, n1:o, n:o
Contexts: Gamma{n, n1, n2, n3, n4, n5, n6}:c[]
IH:
ctx Gamma:c,
forall M1, forall M2, forall T, forall D1, forall D2,
{Gamma |- D1 : step M1 M2}* =>
{Gamma |- D2 : of M1 T} => exists D3, {Gamma |- D3 : of M2 T}
H3:{Gamma |- T1 : ty}*
H4:{Gamma, n:tm |- R1 n : tm}*
H5:{Gamma, n1:tm |- R2 n1 : tm}*
H6:{Gamma, n2:tm, n3:of n2 T1 |- D n2 n3 : step (R1 n2) (R2 n2)}*
H7:{Gamma, n4:tm |- R1 n4 : tm}
H8:{Gamma |- T1 : ty}
H9:{Gamma |- T2 : ty}
H10:{Gamma, n5:tm, n6:of n5 T1 |- D3 n5 n6 : of (R1 n5) T2}
==================================
exists D3, {Gamma |- D3 : of (lam T1 ([c101]R2 c101)) (arr T1 T2)}
Subgoal subject_reduction.2 is:
exists D3, {Gamma |- D3 : of (R N) T}
Subgoal subject_reduction.3 is:
exists D3, {Gamma |- D3 : of (app M N2) T}
Subgoal subject_reduction.4 is:
exists D3, {Gamma |- D3 : of (app M4 N) T}
subject_reduction.1>> apply IH to H6 H10 with (Gamma = Gamma,n1:tm,n:of n1 T1).
Subgoal subject_reduction.1:
Vars: D3:(o) -> (o) -> o, T2:o, D:(o) -> (o) -> o, R1:(o) -> o, T1:o, R2:
(o) -> o, D1:(o) -> (o) -> (o) -> (o) -> (o) -> (o) -> (o) -> o
Nominals: n6:o, n5:o, n4:o, n3:o, n2:o, n1:o, n:o
Contexts: Gamma{n, n1, n2, n3, n4, n5, n6}:c[]
IH:
ctx Gamma:c,
forall M1, forall M2, forall T, forall D1, forall D2,
{Gamma |- D1 : step M1 M2}* =>
{Gamma |- D2 : of M1 T} => exists D3, {Gamma |- D3 : of M2 T}
H3:{Gamma |- T1 : ty}*
H4:{Gamma, n:tm |- R1 n : tm}*
H5:{Gamma, n1:tm |- R2 n1 : tm}*
H6:{Gamma, n2:tm, n3:of n2 T1 |- D n2 n3 : step (R1 n2) (R2 n2)}*
H7:{Gamma, n4:tm |- R1 n4 : tm}
H8:{Gamma |- T1 : ty}
H9:{Gamma |- T2 : ty}
H10:{Gamma, n5:tm, n6:of n5 T1 |- D3 n5 n6 : of (R1 n5) T2}
H11:{Gamma, n1:tm, n:of n1 T1 |- D1 n6 n5 n4 n3 n2 n1 n : of (R2 n1) T2}
==================================
exists D3, {Gamma |- D3 : of (lam T1 ([c101]R2 c101)) (arr T1 T2)}
Subgoal subject_reduction.2 is:
exists D3, {Gamma |- D3 : of (R N) T}
Subgoal subject_reduction.3 is:
exists D3, {Gamma |- D3 : of (app M N2) T}
Subgoal subject_reduction.4 is:
exists D3, {Gamma |- D3 : of (app M4 N) T}
subject_reduction.1>> prune H11.
Subgoal subject_reduction.1:
Vars: D3:(o) -> (o) -> o, T2:o, D:(o) -> (o) -> o, R1:(o) -> o, T1:o, R2:
(o) -> o, D1:(o) -> (o) -> o
Nominals: n6:o, n5:o, n4:o, n3:o, n2:o, n1:o, n:o
Contexts: Gamma{n, n1, n2, n3, n4, n5, n6}:c[]
IH:
ctx Gamma:c,
forall M1, forall M2, forall T, forall D1, forall D2,
{Gamma |- D1 : step M1 M2}* =>
{Gamma |- D2 : of M1 T} => exists D3, {Gamma |- D3 : of M2 T}
H3:{Gamma |- T1 : ty}*
H4:{Gamma, n:tm |- R1 n : tm}*
H5:{Gamma, n1:tm |- R2 n1 : tm}*
H6:{Gamma, n2:tm, n3:of n2 T1 |- D n2 n3 : step (R1 n2) (R2 n2)}*
H7:{Gamma, n4:tm |- R1 n4 : tm}
H8:{Gamma |- T1 : ty}
H9:{Gamma |- T2 : ty}
H10:{Gamma, n5:tm, n6:of n5 T1 |- D3 n5 n6 : of (R1 n5) T2}
H11:{Gamma, n1:tm, n:of n1 T1 |- D1 n1 n : of (R2 n1) T2}
==================================
exists D3, {Gamma |- D3 : of (lam T1 ([c101]R2 c101)) (arr T1 T2)}
Subgoal subject_reduction.2 is:
exists D3, {Gamma |- D3 : of (R N) T}
Subgoal subject_reduction.3 is:
exists D3, {Gamma |- D3 : of (app M N2) T}
Subgoal subject_reduction.4 is:
exists D3, {Gamma |- D3 : of (app M4 N) T}
subject_reduction.1>> exists of_lam ([x]R2 x) T1 T2 ([x][x1]D1 x x1).
Subgoal subject_reduction.1:
Vars: D3:(o) -> (o) -> o, T2:o, D:(o) -> (o) -> o, R1:(o) -> o, T1:o, R2:
(o) -> o, D1:(o) -> (o) -> o
Nominals: n6:o, n5:o, n4:o, n3:o, n2:o, n1:o, n:o
Contexts: Gamma{n, n1, n2, n3, n4, n5, n6}:c[]
IH:
ctx Gamma:c,
forall M1, forall M2, forall T, forall D1, forall D2,
{Gamma |- D1 : step M1 M2}* =>
{Gamma |- D2 : of M1 T} => exists D3, {Gamma |- D3 : of M2 T}
H3:{Gamma |- T1 : ty}*
H4:{Gamma, n:tm |- R1 n : tm}*
H5:{Gamma, n1:tm |- R2 n1 : tm}*
H6:{Gamma, n2:tm, n3:of n2 T1 |- D n2 n3 : step (R1 n2) (R2 n2)}*
H7:{Gamma, n4:tm |- R1 n4 : tm}
H8:{Gamma |- T1 : ty}
H9:{Gamma |- T2 : ty}
H10:{Gamma, n5:tm, n6:of n5 T1 |- D3 n5 n6 : of (R1 n5) T2}
H11:{Gamma, n1:tm, n:of n1 T1 |- D1 n1 n : of (R2 n1) T2}
==================================
{Gamma |- of_lam ([x]R2 x) T1 T2 ([x][x1]D1 x x1) :
of (lam T1 ([c101]R2 c101)) (arr T1 T2)}
Subgoal subject_reduction.2 is:
exists D3, {Gamma |- D3 : of (R N) T}
Subgoal subject_reduction.3 is:
exists D3, {Gamma |- D3 : of (app M N2) T}
Subgoal subject_reduction.4 is:
exists D3, {Gamma |- D3 : of (app M4 N) T}
subject_reduction.1>> search.
Subgoal subject_reduction.2:
Vars: T1:o, R:(o) -> o, N:o, D2:o, T:o
Nominals: n:o
Contexts: Gamma{n}:c[]
IH:
ctx Gamma:c,
forall M1, forall M2, forall T, forall D1, forall D2,
{Gamma |- D1 : step M1 M2}* =>
{Gamma |- D2 : of M1 T} => exists D3, {Gamma |- D3 : of M2 T}
H2:{Gamma |- D2 : of (app (lam T1 ([c22]R c22)) N) T}
H3:{Gamma |- T1 : ty}*
H4:{Gamma, n:tm |- R n : tm}*
H5:{Gamma |- N : tm}*
==================================
exists D3, {Gamma |- D3 : of (R N) T}
Subgoal subject_reduction.3 is:
exists D3, {Gamma |- D3 : of (app M N2) T}
Subgoal subject_reduction.4 is:
exists D3, {Gamma |- D3 : of (app M4 N) T}
subject_reduction.2>> cases H2.
Subgoal subject_reduction.2:
Vars: D3:o, D4:o, D5:o, T1:o, R:(o) -> o, N:o, T:o
Nominals: n:o
Contexts: Gamma{n}:c[]
IH:
ctx Gamma:c,
forall M1, forall M2, forall T, forall D1, forall D2,
{Gamma |- D1 : step M1 M2}* =>
{Gamma |- D2 : of M1 T} => exists D3, {Gamma |- D3 : of M2 T}
H3:{Gamma |- T1 : ty}*
H4:{Gamma, n:tm |- R n : tm}*
H5:{Gamma |- N : tm}*
H6:{Gamma |- lam T1 ([c22]R c22) : tm}
H7:{Gamma |- N : tm}
H8:{Gamma |- T : ty}
H9:{Gamma |- D3 : ty}
H10:{Gamma |- D4 : of (lam T1 ([c22]R c22)) (arr D3 T)}
H11:{Gamma |- D5 : of N D3}
==================================
exists D3, {Gamma |- D3 : of (R N) T}
Subgoal subject_reduction.3 is:
exists D3, {Gamma |- D3 : of (app M N2) T}
Subgoal subject_reduction.4 is:
exists D3, {Gamma |- D3 : of (app M4 N) T}
subject_reduction.2>> cases H10.
Subgoal subject_reduction.2:
Vars: D6:(o) -> (o) -> o, D3:o, D5:o, R:(o) -> o, N:o, T:o
Nominals: n3:o, n2:o, n1:o, n:o
Contexts: Gamma{n, n1, n2, n3}:c[]
IH:
ctx Gamma:c,
forall M1, forall M2, forall T, forall D1, forall D2,
{Gamma |- D1 : step M1 M2}* =>
{Gamma |- D2 : of M1 T} => exists D3, {Gamma |- D3 : of M2 T}
H3:{Gamma |- D3 : ty}*
H4:{Gamma, n:tm |- R n : tm}*
H5:{Gamma |- N : tm}*
H6:{Gamma |- lam D3 ([c22]R c22) : tm}
H7:{Gamma |- N : tm}
H8:{Gamma |- T : ty}
H9:{Gamma |- D3 : ty}
H11:{Gamma |- D5 : of N D3}
H12:{Gamma, n1:tm |- R n1 : tm}
H13:{Gamma |- D3 : ty}
H14:{Gamma |- T : ty}
H15:{Gamma, n2:tm, n3:of n2 D3 |- D6 n2 n3 : of (R n2) T}
==================================
exists D3, {Gamma |- D3 : of (R N) T}
Subgoal subject_reduction.3 is:
exists D3, {Gamma |- D3 : of (app M N2) T}
Subgoal subject_reduction.4 is:
exists D3, {Gamma |- D3 : of (app M4 N) T}
subject_reduction.2>> inst H15 with n2 = N.
Subgoal subject_reduction.2:
Vars: D6:(o) -> (o) -> o, D3:o, D5:o, R:(o) -> o, N:o, T:o
Nominals: n3:o, n2:o, n1:o, n:o
Contexts: Gamma{n, n1, n2, n3}:c[]
IH:
ctx Gamma:c,
forall M1, forall M2, forall T, forall D1, forall D2,
{Gamma |- D1 : step M1 M2}* =>
{Gamma |- D2 : of M1 T} => exists D3, {Gamma |- D3 : of M2 T}
H3:{Gamma |- D3 : ty}*
H4:{Gamma, n:tm |- R n : tm}*
H5:{Gamma |- N : tm}*
H6:{Gamma |- lam D3 ([c22]R c22) : tm}
H7:{Gamma |- N : tm}
H8:{Gamma |- T : ty}
H9:{Gamma |- D3 : ty}
H11:{Gamma |- D5 : of N D3}
H12:{Gamma, n1:tm |- R n1 : tm}
H13:{Gamma |- D3 : ty}
H14:{Gamma |- T : ty}
H15:{Gamma, n2:tm, n3:of n2 D3 |- D6 n2 n3 : of (R n2) T}
H16:{Gamma, n3:of N D3 |- D6 N n3 : of (R N) T}
==================================
exists D3, {Gamma |- D3 : of (R N) T}
Subgoal subject_reduction.3 is:
exists D3, {Gamma |- D3 : of (app M N2) T}
Subgoal subject_reduction.4 is:
exists D3, {Gamma |- D3 : of (app M4 N) T}
subject_reduction.2>> inst H16 with n3 = D5.
Subgoal subject_reduction.2:
Vars: D6:(o) -> (o) -> o, D3:o, D5:o, R:(o) -> o, N:o, T:o
Nominals: n3:o, n2:o, n1:o, n:o
Contexts: Gamma{n, n1, n2, n3}:c[]
IH:
ctx Gamma:c,
forall M1, forall M2, forall T, forall D1, forall D2,
{Gamma |- D1 : step M1 M2}* =>
{Gamma |- D2 : of M1 T} => exists D3, {Gamma |- D3 : of M2 T}
H3:{Gamma |- D3 : ty}*
H4:{Gamma, n:tm |- R n : tm}*
H5:{Gamma |- N : tm}*
H6:{Gamma |- lam D3 ([c22]R c22) : tm}
H7:{Gamma |- N : tm}
H8:{Gamma |- T : ty}
H9:{Gamma |- D3 : ty}
H11:{Gamma |- D5 : of N D3}
H12:{Gamma, n1:tm |- R n1 : tm}
H13:{Gamma |- D3 : ty}
H14:{Gamma |- T : ty}
H15:{Gamma, n2:tm, n3:of n2 D3 |- D6 n2 n3 : of (R n2) T}
H16:{Gamma, n3:of N D3 |- D6 N n3 : of (R N) T}
H17:{Gamma |- D6 N D5 : of (R N) T}
==================================
exists D3, {Gamma |- D3 : of (R N) T}
Subgoal subject_reduction.3 is:
exists D3, {Gamma |- D3 : of (app M N2) T}
Subgoal subject_reduction.4 is:
exists D3, {Gamma |- D3 : of (app M4 N) T}
subject_reduction.2>> exists D6 N D5.
Subgoal subject_reduction.2:
Vars: D6:(o) -> (o) -> o, D3:o, D5:o, R:(o) -> o, N:o, T:o
Nominals: n3:o, n2:o, n1:o, n:o
Contexts: Gamma{n, n1, n2, n3}:c[]
IH:
ctx Gamma:c,
forall M1, forall M2, forall T, forall D1, forall D2,
{Gamma |- D1 : step M1 M2}* =>
{Gamma |- D2 : of M1 T} => exists D3, {Gamma |- D3 : of M2 T}
H3:{Gamma |- D3 : ty}*
H4:{Gamma, n:tm |- R n : tm}*
H5:{Gamma |- N : tm}*
H6:{Gamma |- lam D3 ([c22]R c22) : tm}
H7:{Gamma |- N : tm}
H8:{Gamma |- T : ty}
H9:{Gamma |- D3 : ty}
H11:{Gamma |- D5 : of N D3}
H12:{Gamma, n1:tm |- R n1 : tm}
H13:{Gamma |- D3 : ty}
H14:{Gamma |- T : ty}
H15:{Gamma, n2:tm, n3:of n2 D3 |- D6 n2 n3 : of (R n2) T}
H16:{Gamma, n3:of N D3 |- D6 N n3 : of (R N) T}
H17:{Gamma |- D6 N D5 : of (R N) T}
==================================
{Gamma |- D6 N D5 : of (R N) T}
Subgoal subject_reduction.3 is:
exists D3, {Gamma |- D3 : of (app M N2) T}
Subgoal subject_reduction.4 is:
exists D3, {Gamma |- D3 : of (app M4 N) T}
subject_reduction.2>> search.
Subgoal subject_reduction.3:
Vars: D:o, N1:o, M:o, N2:o, D2:o, T:o
Contexts: Gamma{}:c[]
IH:
ctx Gamma:c,
forall M1, forall M2, forall T, forall D1, forall D2,
{Gamma |- D1 : step M1 M2}* =>
{Gamma |- D2 : of M1 T} => exists D3, {Gamma |- D3 : of M2 T}
H2:{Gamma |- D2 : of (app M N1) T}
H3:{Gamma |- M : tm}*
H4:{Gamma |- N1 : tm}*
H5:{Gamma |- N2 : tm}*
H6:{Gamma |- D : step N1 N2}*
==================================
exists D3, {Gamma |- D3 : of (app M N2) T}
Subgoal subject_reduction.4 is:
exists D3, {Gamma |- D3 : of (app M4 N) T}
subject_reduction.3>> cases H2.
Subgoal subject_reduction.3:
Vars: U:o, a1:o, a2:o, D:o, N1:o, M:o, N2:o, T:o
Contexts: Gamma{}:c[]
IH:
ctx Gamma:c,
forall M1, forall M2, forall T, forall D1, forall D2,
{Gamma |- D1 : step M1 M2}* =>
{Gamma |- D2 : of M1 T} => exists D3, {Gamma |- D3 : of M2 T}
H3:{Gamma |- M : tm}*
H4:{Gamma |- N1 : tm}*
H5:{Gamma |- N2 : tm}*
H6:{Gamma |- D : step N1 N2}*
H7:{Gamma |- M : tm}
H8:{Gamma |- N1 : tm}
H9:{Gamma |- T : ty}
H10:{Gamma |- U : ty}
H11:{Gamma |- a1 : of M (arr U T)}
H12:{Gamma |- a2 : of N1 U}
==================================
exists D3, {Gamma |- D3 : of (app M N2) T}
Subgoal subject_reduction.4 is:
exists D3, {Gamma |- D3 : of (app M4 N) T}
subject_reduction.3>> apply IH to H6 H12.
Subgoal subject_reduction.3:
Vars: D3:o, U:o, a1:o, a2:o, D:o, N1:o, M:o, N2:o, T:o
Contexts: Gamma{}:c[]
IH:
ctx Gamma:c,
forall M1, forall M2, forall T, forall D1, forall D2,
{Gamma |- D1 : step M1 M2}* =>
{Gamma |- D2 : of M1 T} => exists D3, {Gamma |- D3 : of M2 T}
H3:{Gamma |- M : tm}*
H4:{Gamma |- N1 : tm}*
H5:{Gamma |- N2 : tm}*
H6:{Gamma |- D : step N1 N2}*
H7:{Gamma |- M : tm}
H8:{Gamma |- N1 : tm}
H9:{Gamma |- T : ty}
H10:{Gamma |- U : ty}
H11:{Gamma |- a1 : of M (arr U T)}
H12:{Gamma |- a2 : of N1 U}
H13:{Gamma |- D3 : of N2 U}
==================================
exists D3, {Gamma |- D3 : of (app M N2) T}
Subgoal subject_reduction.4 is:
exists D3, {Gamma |- D3 : of (app M4 N) T}
subject_reduction.3>> exists of_app M N2 T U a1 D3.
Subgoal subject_reduction.3:
Vars: D3:o, U:o, a1:o, a2:o, D:o, N1:o, M:o, N2:o, T:o
Contexts: Gamma{}:c[]
IH:
ctx Gamma:c,
forall M1, forall M2, forall T, forall D1, forall D2,
{Gamma |- D1 : step M1 M2}* =>
{Gamma |- D2 : of M1 T} => exists D3, {Gamma |- D3 : of M2 T}
H3:{Gamma |- M : tm}*
H4:{Gamma |- N1 : tm}*
H5:{Gamma |- N2 : tm}*
H6:{Gamma |- D : step N1 N2}*
H7:{Gamma |- M : tm}
H8:{Gamma |- N1 : tm}
H9:{Gamma |- T : ty}
H10:{Gamma |- U : ty}
H11:{Gamma |- a1 : of M (arr U T)}
H12:{Gamma |- a2 : of N1 U}
H13:{Gamma |- D3 : of N2 U}
==================================
{Gamma |- of_app M N2 T U a1 D3 : of (app M N2) T}
Subgoal subject_reduction.4 is:
exists D3, {Gamma |- D3 : of (app M4 N) T}
subject_reduction.3>> search.
Subgoal subject_reduction.4:
Vars: D:o, M3:o, M4:o, N:o, D2:o, T:o
Contexts: Gamma{}:c[]
IH:
ctx Gamma:c,
forall M1, forall M2, forall T, forall D1, forall D2,
{Gamma |- D1 : step M1 M2}* =>
{Gamma |- D2 : of M1 T} => exists D3, {Gamma |- D3 : of M2 T}
H2:{Gamma |- D2 : of (app M3 N) T}
H3:{Gamma |- M3 : tm}*
H4:{Gamma |- M4 : tm}*
H5:{Gamma |- N : tm}*
H6:{Gamma |- D : step M3 M4}*
==================================
exists D3, {Gamma |- D3 : of (app M4 N) T}
subject_reduction.4>> cases H2.
Subgoal subject_reduction.4:
Vars: U:o, a1:o, a2:o, D:o, M3:o, M4:o, N:o, T:o
Contexts: Gamma{}:c[]
IH:
ctx Gamma:c,
forall M1, forall M2, forall T, forall D1, forall D2,
{Gamma |- D1 : step M1 M2}* =>
{Gamma |- D2 : of M1 T} => exists D3, {Gamma |- D3 : of M2 T}
H3:{Gamma |- M3 : tm}*
H4:{Gamma |- M4 : tm}*
H5:{Gamma |- N : tm}*
H6:{Gamma |- D : step M3 M4}*
H7:{Gamma |- M3 : tm}
H8:{Gamma |- N : tm}
H9:{Gamma |- T : ty}
H10:{Gamma |- U : ty}
H11:{Gamma |- a1 : of M3 (arr U T)}
H12:{Gamma |- a2 : of N U}
==================================
exists D3, {Gamma |- D3 : of (app M4 N) T}
subject_reduction.4>> apply IH to H6 H11.
Subgoal subject_reduction.4:
Vars: D3:o, U:o, a1:o, a2:o, D:o, M3:o, M4:o, N:o, T:o
Contexts: Gamma{}:c[]
IH:
ctx Gamma:c,
forall M1, forall M2, forall T, forall D1, forall D2,
{Gamma |- D1 : step M1 M2}* =>
{Gamma |- D2 : of M1 T} => exists D3, {Gamma |- D3 : of M2 T}
H3:{Gamma |- M3 : tm}*
H4:{Gamma |- M4 : tm}*
H5:{Gamma |- N : tm}*
H6:{Gamma |- D : step M3 M4}*
H7:{Gamma |- M3 : tm}
H8:{Gamma |- N : tm}
H9:{Gamma |- T : ty}
H10:{Gamma |- U : ty}
H11:{Gamma |- a1 : of M3 (arr U T)}
H12:{Gamma |- a2 : of N U}
H13:{Gamma |- D3 : of M4 (arr U T)}
==================================
exists D3, {Gamma |- D3 : of (app M4 N) T}
subject_reduction.4>> exists of_app M4 N T U D3 a2.
Subgoal subject_reduction.4:
Vars: D3:o, U:o, a1:o, a2:o, D:o, M3:o, M4:o, N:o, T:o
Contexts: Gamma{}:c[]
IH:
ctx Gamma:c,
forall M1, forall M2, forall T, forall D1, forall D2,
{Gamma |- D1 : step M1 M2}* =>
{Gamma |- D2 : of M1 T} => exists D3, {Gamma |- D3 : of M2 T}
H3:{Gamma |- M3 : tm}*
H4:{Gamma |- M4 : tm}*
H5:{Gamma |- N : tm}*
H6:{Gamma |- D : step M3 M4}*
H7:{Gamma |- M3 : tm}
H8:{Gamma |- N : tm}
H9:{Gamma |- T : ty}
H10:{Gamma |- U : ty}
H11:{Gamma |- a1 : of M3 (arr U T)}
H12:{Gamma |- a2 : of N U}
H13:{Gamma |- D3 : of M4 (arr U T)}
==================================
{Gamma |- of_app M4 N T U D3 a2 : of (app M4 N) T}
subject_reduction.4>> search.
Proof Completed!
>> Goodbye!