- |#P #Hind #N1 #N2 #subH #prH
- (cut (∀S. subterm S (App P N1) → subterm S (App (D P) N1)))
- [#S #sub (cases (subapp …sub)) [* [ * /2/ | /3/] | /2/]] #Hcut
- cases (prApp_D … prH);
- [* #N3 * #eqN3 #pr1 >eqN3 @d @Hind //
- #S #P1 #sub1 #prS @subH /2/
- |* #N3 * #N4 * * #eqN2 #prP #prN1 >eqN2 @dapp @Hind;
- [#S #P1 #sub1 #prS @subH /2/ |@appl // ]
- ]
- ]
-qed.
-
-lemma complete_lam: ∀M,Q,M1.
- (∀S,P.subterm S (Lambda Q M) → pr S P → pr P (full S)) →
- pr (Lambda Q M) M1 → pr M1 (full_lam (full Q) M).
-#M (elim M)
- [#n #Q #M1 #sub #pr1 normalize
- (cases (prLambda_not_dummy … pr1 ?)) // #M2 * #N2
- * * #eqM1 #pr3 #pr4 >eqM1 @lam;
- [@sub /2/ | @(sub (Sort n)) /2/]
- |#n #Q #M1 #sub #pr1 normalize
- (cases (prLambda_not_dummy … pr1 ?)) // #M2 * #N2
- * * #eqM1 #pr3 #pr4 >eqM1 @lam;
- [@sub /2/ | @(sub (Rel n)) /2/]
- |#M1 #M2 #_ #_ #M3 #Q #sub #pr1
- (cases (prLambda_not_dummy … pr1 ?)) // #M4 * #N3
- * * #eqM3 #pr3 #pr4 >eqM3 @lam;
- [@sub // | @complete_app // #S #P1 #subS @sub
- (cases (subapp …subS)) [* [* /2/ | /2/] | /3/ ]
- ]
- |#M1 #M2 #_ #Hind #M3 #Q #sub #pr1
- (cases (prLambda_not_dummy … pr1 ?)) // #M4 * #N3
- * * #eqM3 #pr3 #pr4 >eqM3 @lam;
- [@sub // |@Hind // #S #P1 #subS @sub
- (cases (sublam …subS)) [* [* /2/ | /2/] | /3/ ]
- ]
- |#M1 #M2 #_ #_ #M3 #Q #sub #pr1
- (cases (prLambda_not_dummy … pr1 ?)) // #M4 * #N3
- * * #eqM3 #pr3 #pr4 >eqM3 @lam;
- [@sub // | (cases (prProd … pr4)) #M5 * #N4 * * #eqN3
- #pr5 #pr6 >eqN3 @prod;
- [@sub /3/ | @sub /3/]
- ]
- |#P #Hind #Q #M2 #sub #pr1 (cases (prLambda_dummy … pr1))
- [* #M3 * #N3 * * #eqM2 #pr3 #pr4 >eqM2 normalize
- @dlam @Hind;
- [#S #P1 #subS @sub (cases (sublam …subS))
- [* [* /2/ | /2/ ] |/3/ ]
- |@lam //
- ]
- |* #P * #eqM2 #pr3 >eqM2 normalize @d
- @Hind // #S #P #subH @sub
- (cases (sublam … subH)) [* [* /2/ | /2/] | /3/]
- ]