Subject Reduction for the simply typed lambda-calculus

Specification

ty : type.
top : ty.
arr : {Z1:ty} {Z2:ty} ty.

tm : type.
app : {Y1:tm} {Y2:tm} tm.
lam : {Z:ty} {Y:{x:tm}tm} tm.

of : tm -> ty -> type.
of_app : {M:tm}{N:tm}{T:ty}{U:ty}
          {a1:of M (arr U T)} {a2:of N U} of (app M N) T.
of_lam : {R : {x:tm} tm}{T:ty}{U:ty}
          {a1:({x:tm}{z:of x T} of (R x) U)}
          of (lam T ([x] R x)) (arr T U).

step : tm -> tm -> type.
step-app1 : {M1:tm} {M2:tm} {N:tm} {D : step M1 M2}
            step (app M1 N) (app M2 N).
step-app2 : {M:tm} {N1:tm} {N2:tm} {D : step N1 N2}
            step (app M N1) (app M N2).
step-beta : {T:ty} {R:{x:tm}tm} {N:tm}
            step (app (lam T ([x] R x)) N) (R N).
step-lam  : {T:ty} {R1:{x:tm}tm} {R2:{x:tm}tm}
            {D : {x:tm} {d:of x T} step (R1 x) (R2 x)}
            step (lam T ([x] R1 x)) (lam T ([x] R2 x)).

Reasoning

%Completed as part of Daniel Luick's honors thesis which can be accessed here. 

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}.

  induction on 1. intros. case H1.

  % step-lam case
  case H2.
  apply IH to H6 H10 with (Gamma = Gamma, n1:tm, n:of n1 T1).
  prune H11.
  exists of_lam ([x] R2 x) T1 T2 ([x] [x1] D1 x x1).
  search.

  % step-beta case
  case H2.
  case H10.
  inst H15 with n2 = N.
  inst H16 with n3 = D5.
  exists D6 N D5.
  search.

  % step-app2 case
  case H2.
  apply IH to H6 H12.
  exists of_app M N2 T U a1 D3.
  search.

  % step-app1 case
  case H2.
  apply IH to H6 H11.
  exists of_app M4 N T U D3 a2.
  search.