Strengthening in Simply Typed $\lambda$-Calculus

stren.lf

tp : type.
arr : {T:tp}{U:tp}tp.
unit : tp.
 
tm : type.
empty : tm.
app : {E1:tm}{E2:tm}tm.
abs : {T:tp}{E:{x:tm}tm}tm.
 
of : {E:tm}{T:tp}type.
of-abs : {U:tp}{T:tp}{E:{x:tm} tm}
          {D:({x:tm}{z:of x U} of (E x) T)}
          of (abs U ([x] E x)) (arr U T).
of-app : {E1:tm}{E2:tm}{U:tp}{T:tp}
          {D1:of E1 (arr U T)} {D2:of E2 U} of (app E1 E2) T.
of-empty : of empty unit.

stren.ath

Specification "stren.lf".
 
Schema c :=
 {T}(x:tm,y:of x T).
 
Theorem stren : ctx G:c, forall E T1 T2 D: o -> o -> o,
  { G |- [x][dx] D x dx : {x:tm}{dx: of x T2} of E T1 } =>
    exists D', { G |- D' : of E T1 }.
induction on 1. intros.
case H1 (keep).
  % of-empty
  exists of-empty. search.
  % of-app
  prune H4.
  apply IH to H6. apply IH to H7.
  prune H8. prune H9.
  exists of-app E1 E2 U T1 D' D'1. search.
  % of-abs
  ctxpermute H5 to G, n3:tm, n4:of n3 E1, n:tm, n1:of n T2.
  apply IH to H6 with (G = G, n1:tm, n: of n1 E1). prune H7.
  assert { G |- E1 : tp }*. strengthen H2. strengthen H8. search.
  assert { G |- T3 : tp }*. strengthen H3. strengthen H9. search.
  assert { G, n:tm, n1:of n E1 |- E2 n : tm }. strengthen H10.
  exists of-abs E1 T3 E2 D'. search.
  % var
  exists n3. search.