]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/sn3/props.ma
exercise ready
[helm.git] / helm / software / matita / contribs / LAMBDA-TYPES / LambdaDelta-1 / sn3 / props.ma
index afd3fdbc9b1e8cd817757bea39f46480049c5fef..cf432cbfc2434f56f7c57d7a7fc51ffbdfbf5e11 100644 (file)
 
 (* This file was automatically generated: do not edit *********************)
 
-include "sn3/nf2.ma".
+include "LambdaDelta-1/sn3/nf2.ma".
 
-include "sn3/fwd.ma".
+include "LambdaDelta-1/sn3/fwd.ma".
 
-include "nf2/iso.ma".
+include "LambdaDelta-1/nf2/iso.ma".
 
-include "pr3/iso.ma".
-
-include "iso/props.ma".
+include "LambdaDelta-1/pr3/iso.ma".
 
 theorem sn3_pr3_trans:
  \forall (c: C).(\forall (t1: T).((sn3 c t1) \to (\forall (t2: T).((pr3 c t1 
@@ -159,7 +157,7 @@ theorem sn3_shift:
 \def
  \lambda (b: B).(\lambda (c: C).(\lambda (v: T).(\lambda (t: T).(\lambda (H: 
 (sn3 c (THead (Bind b) v t))).(let H_x \def (sn3_gen_bind b c v t H) in (let 
-H0 \def H_x in (and_ind (sn3 c v) (sn3 (CHead c (Bind b) v) t) (sn3 (CHead c 
+H0 \def H_x in (land_ind (sn3 c v) (sn3 (CHead c (Bind b) v) t) (sn3 (CHead c 
 (Bind b) v) t) (\lambda (_: (sn3 c v)).(\lambda (H2: (sn3 (CHead c (Bind b) 
 v) t)).H2)) H0))))))).
 
@@ -181,6 +179,71 @@ Prop).P)))).(\lambda (H4: (pr2 (CHead c (Bind b) v2) t1 t2)).(H2 t2 H3
 (pr3_pr2 (CHead c (Bind b) v1) t1 t2 (pr2_change b H c v2 t1 t2 H4 
 v1)))))))))) t H0))))))).
 
+theorem sn3_gen_def:
+ \forall (c: C).(\forall (d: C).(\forall (v: T).(\forall (i: nat).((getl i c 
+(CHead d (Bind Abbr) v)) \to ((sn3 c (TLRef i)) \to (sn3 d v))))))
+\def
+ \lambda (c: C).(\lambda (d: C).(\lambda (v: T).(\lambda (i: nat).(\lambda 
+(H: (getl i c (CHead d (Bind Abbr) v))).(\lambda (H0: (sn3 c (TLRef 
+i))).(sn3_gen_lift c v (S i) O (sn3_pr3_trans c (TLRef i) H0 (lift (S i) O v) 
+(pr3_pr2 c (TLRef i) (lift (S i) O v) (pr2_delta c d v i H (TLRef i) (TLRef 
+i) (pr0_refl (TLRef i)) (lift (S i) O v) (subst0_lref v i)))) d (getl_drop 
+Abbr c d v i H))))))).
+
+theorem sn3_cdelta:
+ \forall (v: T).(\forall (t: T).(\forall (i: nat).(((\forall (w: T).(ex T 
+(\lambda (u: T).(subst0 i w t u))))) \to (\forall (c: C).(\forall (d: 
+C).((getl i c (CHead d (Bind Abbr) v)) \to ((sn3 c t) \to (sn3 d v))))))))
+\def
+ \lambda (v: T).(\lambda (t: T).(\lambda (i: nat).(\lambda (H: ((\forall (w: 
+T).(ex T (\lambda (u: T).(subst0 i w t u)))))).(let H_x \def (H v) in (let H0 
+\def H_x in (ex_ind T (\lambda (u: T).(subst0 i v t u)) (\forall (c: 
+C).(\forall (d: C).((getl i c (CHead d (Bind Abbr) v)) \to ((sn3 c t) \to 
+(sn3 d v))))) (\lambda (x: T).(\lambda (H1: (subst0 i v t x)).(subst0_ind 
+(\lambda (n: nat).(\lambda (t0: T).(\lambda (t1: T).(\lambda (_: T).(\forall 
+(c: C).(\forall (d: C).((getl n c (CHead d (Bind Abbr) t0)) \to ((sn3 c t1) 
+\to (sn3 d t0))))))))) (\lambda (v0: T).(\lambda (i0: nat).(\lambda (c: 
+C).(\lambda (d: C).(\lambda (H2: (getl i0 c (CHead d (Bind Abbr) 
+v0))).(\lambda (H3: (sn3 c (TLRef i0))).(sn3_gen_def c d v0 i0 H2 H3))))))) 
+(\lambda (v0: T).(\lambda (u2: T).(\lambda (u1: T).(\lambda (i0: 
+nat).(\lambda (_: (subst0 i0 v0 u1 u2)).(\lambda (H3: ((\forall (c: 
+C).(\forall (d: C).((getl i0 c (CHead d (Bind Abbr) v0)) \to ((sn3 c u1) \to 
+(sn3 d v0))))))).(\lambda (t0: T).(\lambda (k: K).(\lambda (c: C).(\lambda 
+(d: C).(\lambda (H4: (getl i0 c (CHead d (Bind Abbr) v0))).(\lambda (H5: (sn3 
+c (THead k u1 t0))).(let H_y \def (sn3_gen_head k c u1 t0 H5) in (H3 c d H4 
+H_y)))))))))))))) (\lambda (k: K).(\lambda (v0: T).(\lambda (t2: T).(\lambda 
+(t1: T).(\lambda (i0: nat).(\lambda (H2: (subst0 (s k i0) v0 t1 t2)).(\lambda 
+(H3: ((\forall (c: C).(\forall (d: C).((getl (s k i0) c (CHead d (Bind Abbr) 
+v0)) \to ((sn3 c t1) \to (sn3 d v0))))))).(\lambda (u: T).(\lambda (c: 
+C).(\lambda (d: C).(\lambda (H4: (getl i0 c (CHead d (Bind Abbr) 
+v0))).(\lambda (H5: (sn3 c (THead k u t1))).(K_ind (\lambda (k0: K).((subst0 
+(s k0 i0) v0 t1 t2) \to (((\forall (c0: C).(\forall (d0: C).((getl (s k0 i0) 
+c0 (CHead d0 (Bind Abbr) v0)) \to ((sn3 c0 t1) \to (sn3 d0 v0)))))) \to ((sn3 
+c (THead k0 u t1)) \to (sn3 d v0))))) (\lambda (b: B).(\lambda (_: (subst0 (s 
+(Bind b) i0) v0 t1 t2)).(\lambda (H7: ((\forall (c0: C).(\forall (d0: 
+C).((getl (s (Bind b) i0) c0 (CHead d0 (Bind Abbr) v0)) \to ((sn3 c0 t1) \to 
+(sn3 d0 v0))))))).(\lambda (H8: (sn3 c (THead (Bind b) u t1))).(let H_x0 \def 
+(sn3_gen_bind b c u t1 H8) in (let H9 \def H_x0 in (land_ind (sn3 c u) (sn3 
+(CHead c (Bind b) u) t1) (sn3 d v0) (\lambda (_: (sn3 c u)).(\lambda (H11: 
+(sn3 (CHead c (Bind b) u) t1)).(H7 (CHead c (Bind b) u) d (getl_clear_bind b 
+(CHead c (Bind b) u) c u (clear_bind b c u) (CHead d (Bind Abbr) v0) i0 H4) 
+H11))) H9))))))) (\lambda (f: F).(\lambda (_: (subst0 (s (Flat f) i0) v0 t1 
+t2)).(\lambda (H7: ((\forall (c0: C).(\forall (d0: C).((getl (s (Flat f) i0) 
+c0 (CHead d0 (Bind Abbr) v0)) \to ((sn3 c0 t1) \to (sn3 d0 v0))))))).(\lambda 
+(H8: (sn3 c (THead (Flat f) u t1))).(let H_x0 \def (sn3_gen_flat f c u t1 H8) 
+in (let H9 \def H_x0 in (land_ind (sn3 c u) (sn3 c t1) (sn3 d v0) (\lambda 
+(_: (sn3 c u)).(\lambda (H11: (sn3 c t1)).(H7 c d H4 H11))) H9))))))) k H2 H3 
+H5))))))))))))) (\lambda (v0: T).(\lambda (u1: T).(\lambda (u2: T).(\lambda 
+(i0: nat).(\lambda (_: (subst0 i0 v0 u1 u2)).(\lambda (H3: ((\forall (c: 
+C).(\forall (d: C).((getl i0 c (CHead d (Bind Abbr) v0)) \to ((sn3 c u1) \to 
+(sn3 d v0))))))).(\lambda (k: K).(\lambda (t1: T).(\lambda (t2: T).(\lambda 
+(_: (subst0 (s k i0) v0 t1 t2)).(\lambda (_: ((\forall (c: C).(\forall (d: 
+C).((getl (s k i0) c (CHead d (Bind Abbr) v0)) \to ((sn3 c t1) \to (sn3 d 
+v0))))))).(\lambda (c: C).(\lambda (d: C).(\lambda (H6: (getl i0 c (CHead d 
+(Bind Abbr) v0))).(\lambda (H7: (sn3 c (THead k u1 t1))).(let H_y \def 
+(sn3_gen_head k c u1 t1 H7) in (H3 c d H6 H_y))))))))))))))))) i v t x H1))) 
+H0)))))).
+
 theorem sn3_cpr3_trans:
  \forall (c: C).(\forall (u1: T).(\forall (u2: T).((pr3 c u1 u2) \to (\forall 
 (k: K).(\forall (t: T).((sn3 (CHead c k u1) t) \to (sn3 (CHead c k u2) 
@@ -307,11 +370,9 @@ T t2 x1) \to (\forall (P: Prop).P)))).(H1 x0 H16 H12 x1 (sn3_cpr3_trans c t1
 x0 H12 (Bind b) x1 (H3 x1 H18 H13)))) H17)))) H15))) t3 H11))))))) H10)) 
 (\lambda (H10: (pr3 (CHead c (Bind b) t1) t2 (lift (S O) O 
 t3))).(sn3_gen_lift (CHead c (Bind b) t1) t3 (S O) O (sn3_pr3_trans (CHead c 
-(Bind b) t1) t2 (sn3_pr2_intro (CHead c (Bind b) t1) t2 (\lambda (t0: 
-T).(\lambda (H11: (((eq T t2 t0) \to (\forall (P: Prop).P)))).(\lambda (H12: 
-(pr2 (CHead c (Bind b) t1) t2 t0)).(H3 t0 H11 (pr3_pr2 (CHead c (Bind b) t1) 
-t2 t0 H12)))))) (lift (S O) O t3) H10) c (drop_drop (Bind b) O c c (drop_refl 
-c) t1))) H9)))) H7)))))))))) t H2)))))) u H)))).
+(Bind b) t1) t2 (sn3_sing (CHead c (Bind b) t1) t2 H3) (lift (S O) O t3) H10) 
+c (drop_drop (Bind b) O c c (drop_refl c) t1))) H9)))) H7)))))))))) t 
+H2)))))) u H)))).
 
 theorem sn3_beta:
  \forall (c: C).(\forall (v: T).(\forall (t: T).((sn3 c (THead (Bind Abbr) v 
@@ -2104,7 +2165,7 @@ t))))))))))
  \lambda (c: C).(\lambda (u: T).(\lambda (v: T).(\lambda (t: T).(\lambda (H: 
 (sn3 c (THead (Flat Appl) u (THead (Bind Abbr) v t)))).(\lambda (w: 
 T).(\lambda (H0: (sn3 c w)).(let H_x \def (sn3_gen_flat Appl c u (THead (Bind 
-Abbr) v t) H) in (let H1 \def H_x in (and_ind (sn3 c u) (sn3 c (THead (Bind 
+Abbr) v t) H) in (let H1 \def H_x in (land_ind (sn3 c u) (sn3 c (THead (Bind 
 Abbr) v t)) (sn3 c (THead (Flat Appl) u (THead (Flat Appl) v (THead (Bind 
 Abst) w t)))) (\lambda (H2: (sn3 c u)).(\lambda (H3: (sn3 c (THead (Bind 
 Abbr) v t))).(sn3_appl_appl v (THead (Bind Abst) w t) c (sn3_beta c v t H3 w 
@@ -2143,17 +2204,17 @@ c t1) \to (sn3 c (THeads (Flat Appl) t1 (TLRef i))))) \to ((land (sn3 c t)
 (sns3 c t1)) \to (sn3 c (THead (Flat Appl) t (THeads (Flat Appl) t1 (TLRef 
 i))))))) (\lambda (_: (((sns3 c TNil) \to (sn3 c (THeads (Flat Appl) TNil 
 (TLRef i)))))).(\lambda (H1: (land (sn3 c t) (sns3 c TNil))).(let H2 \def H1 
-in (and_ind (sn3 c t) True (sn3 c (THead (Flat Appl) t (THeads (Flat Appl) 
+in (land_ind (sn3 c t) True (sn3 c (THead (Flat Appl) t (THeads (Flat Appl) 
 TNil (TLRef i)))) (\lambda (H3: (sn3 c t)).(\lambda (_: True).(sn3_appl_lref 
 c i H t H3))) H2)))) (\lambda (t1: T).(\lambda (t2: TList).(\lambda (_: 
 (((((sns3 c t2) \to (sn3 c (THeads (Flat Appl) t2 (TLRef i))))) \to ((land 
 (sn3 c t) (sns3 c t2)) \to (sn3 c (THead (Flat Appl) t (THeads (Flat Appl) t2 
 (TLRef i)))))))).(\lambda (H1: (((sns3 c (TCons t1 t2)) \to (sn3 c (THeads 
 (Flat Appl) (TCons t1 t2) (TLRef i)))))).(\lambda (H2: (land (sn3 c t) (sns3 
-c (TCons t1 t2)))).(let H3 \def H2 in (and_ind (sn3 c t) (land (sn3 c t1) 
+c (TCons t1 t2)))).(let H3 \def H2 in (land_ind (sn3 c t) (land (sn3 c t1) 
 (sns3 c t2)) (sn3 c (THead (Flat Appl) t (THeads (Flat Appl) (TCons t1 t2) 
 (TLRef i)))) (\lambda (H4: (sn3 c t)).(\lambda (H5: (land (sn3 c t1) (sns3 c 
-t2))).(and_ind (sn3 c t1) (sns3 c t2) (sn3 c (THead (Flat Appl) t (THeads 
+t2))).(land_ind (sn3 c t1) (sns3 c t2) (sn3 c (THead (Flat Appl) t (THeads 
 (Flat Appl) (TCons t1 t2) (TLRef i)))) (\lambda (H6: (sn3 c t1)).(\lambda 
 (H7: (sns3 c t2)).(sn3_appl_appls t1 (TLRef i) t2 c (H1 (conj (sn3 c t1) 
 (sns3 c t2) H6 H7)) t H4 (\lambda (u2: T).(\lambda (H8: (pr3 c (THeads (Flat 
@@ -2197,22 +2258,23 @@ t3))))))))).(\lambda (u: T).(\lambda (H1: (sn3 c (THead (Flat Appl) t (THeads
 (Flat Appl) (TCons t1 t2) u)))).(\lambda (t3: T).(\lambda (H2: (sn3 c (THead 
 (Flat Appl) t (THeads (Flat Appl) (TCons t1 t2) t3)))).(let H_x \def 
 (sn3_gen_flat Appl c t (THeads (Flat Appl) (TCons t1 t2) t3) H2) in (let H3 
-\def H_x in (and_ind (sn3 c t) (sn3 c (THeads (Flat Appl) (TCons t1 t2) t3)) 
-(sn3 c (THead (Flat Appl) t (THeads (Flat Appl) (TCons t1 t2) (THead (Flat 
-Cast) u t3)))) (\lambda (_: (sn3 c t)).(\lambda (H5: (sn3 c (THeads (Flat 
-Appl) (TCons t1 t2) t3))).(let H6 \def H5 in (let H_x0 \def (sn3_gen_flat 
-Appl c t (THeads (Flat Appl) (TCons t1 t2) u) H1) in (let H7 \def H_x0 in 
-(and_ind (sn3 c t) (sn3 c (THeads (Flat Appl) (TCons t1 t2) u)) (sn3 c (THead 
-(Flat Appl) t (THeads (Flat Appl) (TCons t1 t2) (THead (Flat Cast) u t3)))) 
-(\lambda (H8: (sn3 c t)).(\lambda (H9: (sn3 c (THeads (Flat Appl) (TCons t1 
-t2) u))).(let H10 \def H9 in (sn3_appl_appls t1 (THead (Flat Cast) u t3) t2 c 
-(H0 u H10 t3 H6) t H8 (\lambda (u2: T).(\lambda (H11: (pr3 c (THeads (Flat 
-Appl) (TCons t1 t2) (THead (Flat Cast) u t3)) u2)).(\lambda (H12: (((iso 
-(THeads (Flat Appl) (TCons t1 t2) (THead (Flat Cast) u t3)) u2) \to (\forall 
-(P: Prop).P)))).(sn3_pr3_trans c (THead (Flat Appl) t (THeads (Flat Appl) 
-(TCons t1 t2) t3)) H2 (THead (Flat Appl) t u2) (pr3_thin_dx c (THeads (Flat 
-Appl) (TCons t1 t2) t3) u2 (pr3_iso_appls_cast c u t3 (TCons t1 t2) u2 H11 
-H12) t Appl))))))))) H7)))))) H3))))))))))) t0))) vs)).
+\def H_x in (land_ind (sn3 c t) (sn3 c (THead (Flat Appl) t1 (THeads (Flat 
+Appl) t2 t3))) (sn3 c (THead (Flat Appl) t (THeads (Flat Appl) (TCons t1 t2) 
+(THead (Flat Cast) u t3)))) (\lambda (_: (sn3 c t)).(\lambda (H5: (sn3 c 
+(THead (Flat Appl) t1 (THeads (Flat Appl) t2 t3)))).(let H6 \def H5 in (let 
+H_x0 \def (sn3_gen_flat Appl c t (THeads (Flat Appl) (TCons t1 t2) u) H1) in 
+(let H7 \def H_x0 in (land_ind (sn3 c t) (sn3 c (THead (Flat Appl) t1 (THeads 
+(Flat Appl) t2 u))) (sn3 c (THead (Flat Appl) t (THeads (Flat Appl) (TCons t1 
+t2) (THead (Flat Cast) u t3)))) (\lambda (H8: (sn3 c t)).(\lambda (H9: (sn3 c 
+(THead (Flat Appl) t1 (THeads (Flat Appl) t2 u)))).(let H10 \def H9 in 
+(sn3_appl_appls t1 (THead (Flat Cast) u t3) t2 c (H0 u H10 t3 H6) t H8 
+(\lambda (u2: T).(\lambda (H11: (pr3 c (THeads (Flat Appl) (TCons t1 t2) 
+(THead (Flat Cast) u t3)) u2)).(\lambda (H12: (((iso (THeads (Flat Appl) 
+(TCons t1 t2) (THead (Flat Cast) u t3)) u2) \to (\forall (P: 
+Prop).P)))).(sn3_pr3_trans c (THead (Flat Appl) t (THeads (Flat Appl) (TCons 
+t1 t2) t3)) H2 (THead (Flat Appl) t u2) (pr3_thin_dx c (THeads (Flat Appl) 
+(TCons t1 t2) t3) u2 (pr3_iso_appls_cast c u t3 (TCons t1 t2) u2 H11 H12) t 
+Appl))))))))) H7)))))) H3))))))))))) t0))) vs)).
 
 theorem sn3_appls_bind:
  \forall (b: B).((not (eq B b Abst)) \to (\forall (c: C).(\forall (u: 
@@ -2247,23 +2309,24 @@ t1))))))))).(\lambda (H2: ((\forall (t1: T).((sn3 (CHead c (Bind b) u)
 T).(\lambda (H3: (sn3 (CHead c (Bind b) u) (THead (Flat Appl) (lift (S O) O 
 v) (THeads (Flat Appl) (lifts (S O) O (TCons t t0)) t1)))).(let H_x \def 
 (sn3_gen_flat Appl (CHead c (Bind b) u) (lift (S O) O v) (THeads (Flat Appl) 
-(lifts (S O) O (TCons t t0)) t1) H3) in (let H4 \def H_x in (and_ind (sn3 
-(CHead c (Bind b) u) (lift (S O) O v)) (sn3 (CHead c (Bind b) u) (THeads 
-(Flat Appl) (lifts (S O) O (TCons t t0)) t1)) (sn3 c (THead (Flat Appl) v 
-(THeads (Flat Appl) (TCons t t0) (THead (Bind b) u t1)))) (\lambda (H5: (sn3 
-(CHead c (Bind b) u) (lift (S O) O v))).(\lambda (H6: (sn3 (CHead c (Bind b) 
-u) (THeads (Flat Appl) (lifts (S O) O (TCons t t0)) t1))).(let H_y \def 
-(sn3_gen_lift (CHead c (Bind b) u) v (S O) O H5 c) in (sn3_appl_appls t 
-(THead (Bind b) u t1) t0 c (H2 t1 H6) v (H_y (drop_drop (Bind b) O c c 
-(drop_refl c) u)) (\lambda (u2: T).(\lambda (H7: (pr3 c (THeads (Flat Appl) 
-(TCons t t0) (THead (Bind b) u t1)) u2)).(\lambda (H8: (((iso (THeads (Flat 
-Appl) (TCons t t0) (THead (Bind b) u t1)) u2) \to (\forall (P: 
-Prop).P)))).(let H9 \def (pr3_iso_appls_bind b H (TCons t t0) u t1 c u2 H7 
-H8) in (sn3_pr3_trans c (THead (Flat Appl) v (THead (Bind b) u (THeads (Flat 
-Appl) (lifts (S O) O (TCons t t0)) t1))) (sn3_appl_bind b H c u H0 (THeads 
-(Flat Appl) (lifts (S O) O (TCons t t0)) t1) v H3) (THead (Flat Appl) v u2) 
-(pr3_flat c v v (pr3_refl c v) (THead (Bind b) u (THeads (Flat Appl) (lifts 
-(S O) O (TCons t t0)) t1)) u2 H9 Appl)))))))))) H4))))))))) vs0))) vs)))))).
+(lifts (S O) O (TCons t t0)) t1) H3) in (let H4 \def H_x in (land_ind (sn3 
+(CHead c (Bind b) u) (lift (S O) O v)) (sn3 (CHead c (Bind b) u) (THead (Flat 
+Appl) (lift (S O) O t) (THeads (Flat Appl) (lifts (S O) O t0) t1))) (sn3 c 
+(THead (Flat Appl) v (THeads (Flat Appl) (TCons t t0) (THead (Bind b) u 
+t1)))) (\lambda (H5: (sn3 (CHead c (Bind b) u) (lift (S O) O v))).(\lambda 
+(H6: (sn3 (CHead c (Bind b) u) (THead (Flat Appl) (lift (S O) O t) (THeads 
+(Flat Appl) (lifts (S O) O t0) t1)))).(let H_y \def (sn3_gen_lift (CHead c 
+(Bind b) u) v (S O) O H5 c) in (sn3_appl_appls t (THead (Bind b) u t1) t0 c 
+(H2 t1 H6) v (H_y (drop_drop (Bind b) O c c (drop_refl c) u)) (\lambda (u2: 
+T).(\lambda (H7: (pr3 c (THeads (Flat Appl) (TCons t t0) (THead (Bind b) u 
+t1)) u2)).(\lambda (H8: (((iso (THeads (Flat Appl) (TCons t t0) (THead (Bind 
+b) u t1)) u2) \to (\forall (P: Prop).P)))).(let H9 \def (pr3_iso_appls_bind b 
+H (TCons t t0) u t1 c u2 H7 H8) in (sn3_pr3_trans c (THead (Flat Appl) v 
+(THead (Bind b) u (THeads (Flat Appl) (lifts (S O) O (TCons t t0)) t1))) 
+(sn3_appl_bind b H c u H0 (THeads (Flat Appl) (lifts (S O) O (TCons t t0)) 
+t1) v H3) (THead (Flat Appl) v u2) (pr3_flat c v v (pr3_refl c v) (THead 
+(Bind b) u (THeads (Flat Appl) (lifts (S O) O (TCons t t0)) t1)) u2 H9 
+Appl)))))))))) H4))))))))) vs0))) vs)))))).
 
 theorem sn3_appls_beta:
  \forall (c: C).(\forall (v: T).(\forall (t: T).(\forall (us: TList).((sn3 c 
@@ -2300,16 +2363,16 @@ Appl) (TCons t0 t1) (THead (Bind Abbr) v t))) \to (\forall (w: T).((sn3 c w)
 (Flat Appl) (TCons t0 t1) (THead (Bind Abbr) v t))))).(\lambda (w: 
 T).(\lambda (H2: (sn3 c w)).(let H_x \def (sn3_gen_flat Appl c u (THeads 
 (Flat Appl) (TCons t0 t1) (THead (Bind Abbr) v t)) H1) in (let H3 \def H_x in 
-(and_ind (sn3 c u) (sn3 c (THeads (Flat Appl) (TCons t0 t1) (THead (Bind 
-Abbr) v t))) (sn3 c (THead (Flat Appl) u (THeads (Flat Appl) (TCons t0 t1
-(THead (Flat Appl) v (THead (Bind Abst) w t))))) (\lambda (H4: (sn3 c 
-u)).(\lambda (H5: (sn3 c (THeads (Flat Appl) (TCons t0 t1) (THead (Bind Abbr) 
-v t)))).(sn3_appl_appls t0 (THead (Flat Appl) v (THead (Bind Abst) w t)) t1 c 
-(H0 H5 w H2) u H4 (\lambda (u2: T).(\lambda (H6: (pr3 c (THeads (Flat Appl) 
-(TCons t0 t1) (THead (Flat Appl) v (THead (Bind Abst) w t))) u2)).(\lambda 
-(H7: (((iso (THeads (Flat Appl) (TCons t0 t1) (THead (Flat Appl) v (THead 
-(Bind Abst) w t))) u2) \to (\forall (P: Prop).P)))).(let H8 \def 
-(pr3_iso_appls_beta (TCons t0 t1) v w t c u2 H6 H7) in (sn3_pr3_trans c 
+(land_ind (sn3 c u) (sn3 c (THead (Flat Appl) t0 (THeads (Flat Appl) t1 
+(THead (Bind Abbr) v t)))) (sn3 c (THead (Flat Appl) u (THeads (Flat Appl
+(TCons t0 t1) (THead (Flat Appl) v (THead (Bind Abst) w t))))) (\lambda (H4: 
+(sn3 c u)).(\lambda (H5: (sn3 c (THead (Flat Appl) t0 (THeads (Flat Appl) t1 
+(THead (Bind Abbr) v t))))).(sn3_appl_appls t0 (THead (Flat Appl) v (THead 
+(Bind Abst) w t)) t1 c (H0 H5 w H2) u H4 (\lambda (u2: T).(\lambda (H6: (pr3 
+c (THeads (Flat Appl) (TCons t0 t1) (THead (Flat Appl) v (THead (Bind Abst) w 
+t))) u2)).(\lambda (H7: (((iso (THeads (Flat Appl) (TCons t0 t1) (THead (Flat 
+Appl) v (THead (Bind Abst) w t))) u2) \to (\forall (P: Prop).P)))).(let H8 
+\def (pr3_iso_appls_beta (TCons t0 t1) v w t c u2 H6 H7) in (sn3_pr3_trans c 
 (THead (Flat Appl) u (THeads (Flat Appl) (TCons t0 t1) (THead (Bind Abbr) v 
 t))) H1 (THead (Flat Appl) u u2) (pr3_thin_dx c (THeads (Flat Appl) (TCons t0 
 t1) (THead (Bind Abbr) v t)) u2 H8 u Appl))))))))) H3)))))))))) us0))) us)))).
@@ -2405,17 +2468,18 @@ i)))))))).(\lambda (H1: (((sn3 c (THeads (Flat Appl) (TCons t t0) (lift (S i)
 O w))) \to (sn3 c (THeads (Flat Appl) (TCons t t0) (TLRef i)))))).(\lambda 
 (H2: (sn3 c (THead (Flat Appl) v (THeads (Flat Appl) (TCons t t0) (lift (S i) 
 O w))))).(let H_x \def (sn3_gen_flat Appl c v (THeads (Flat Appl) (TCons t 
-t0) (lift (S i) O w)) H2) in (let H3 \def H_x in (and_ind (sn3 c v) (sn3 c 
-(THeads (Flat Appl) (TCons t t0) (lift (S i) O w))) (sn3 c (THead (Flat Appl) 
-v (THeads (Flat Appl) (TCons t t0) (TLRef i)))) (\lambda (H4: (sn3 c 
-v)).(\lambda (H5: (sn3 c (THeads (Flat Appl) (TCons t t0) (lift (S i) O 
-w)))).(sn3_appl_appls t (TLRef i) t0 c (H1 H5) v H4 (\lambda (u2: T).(\lambda 
-(H6: (pr3 c (THeads (Flat Appl) (TCons t t0) (TLRef i)) u2)).(\lambda (H7: 
-(((iso (THeads (Flat Appl) (TCons t t0) (TLRef i)) u2) \to (\forall (P: 
-Prop).P)))).(sn3_pr3_trans c (THead (Flat Appl) v (THeads (Flat Appl) (TCons 
-t t0) (lift (S i) O w))) H2 (THead (Flat Appl) v u2) (pr3_thin_dx c (THeads 
-(Flat Appl) (TCons t t0) (lift (S i) O w)) u2 (pr3_iso_appls_abbr c d w i H 
-(TCons t t0) u2 H6 H7) v Appl)))))))) H3)))))))) vs0))) vs)))))).
+t0) (lift (S i) O w)) H2) in (let H3 \def H_x in (land_ind (sn3 c v) (sn3 c 
+(THead (Flat Appl) t (THeads (Flat Appl) t0 (lift (S i) O w)))) (sn3 c (THead 
+(Flat Appl) v (THeads (Flat Appl) (TCons t t0) (TLRef i)))) (\lambda (H4: 
+(sn3 c v)).(\lambda (H5: (sn3 c (THead (Flat Appl) t (THeads (Flat Appl) t0 
+(lift (S i) O w))))).(sn3_appl_appls t (TLRef i) t0 c (H1 H5) v H4 (\lambda 
+(u2: T).(\lambda (H6: (pr3 c (THeads (Flat Appl) (TCons t t0) (TLRef i)) 
+u2)).(\lambda (H7: (((iso (THeads (Flat Appl) (TCons t t0) (TLRef i)) u2) \to 
+(\forall (P: Prop).P)))).(sn3_pr3_trans c (THead (Flat Appl) v (THeads (Flat 
+Appl) (TCons t t0) (lift (S i) O w))) H2 (THead (Flat Appl) v u2) 
+(pr3_thin_dx c (THeads (Flat Appl) (TCons t t0) (lift (S i) O w)) u2 
+(pr3_iso_appls_abbr c d w i H (TCons t t0) u2 H6 H7) v Appl)))))))) 
+H3)))))))) vs0))) vs)))))).
 
 theorem sns3_lifts:
  \forall (c: C).(\forall (d: C).(\forall (h: nat).(\forall (i: nat).((drop h 
@@ -2426,73 +2490,8 @@ i c d) \to (\forall (ts: TList).((sns3 d ts) \to (sns3 c (lifts h i ts))))))))
 TList).((sns3 d t) \to (sns3 c (lifts h i t)))) (\lambda (H0: True).H0) 
 (\lambda (t: T).(\lambda (t0: TList).(\lambda (H0: (((sns3 d t0) \to (sns3 c 
 (lifts h i t0))))).(\lambda (H1: (land (sn3 d t) (sns3 d t0))).(let H2 \def 
-H1 in (and_ind (sn3 d t) (sns3 d t0) (land (sn3 c (lift h i t)) (sns3 c 
+H1 in (land_ind (sn3 d t) (sns3 d t0) (land (sn3 c (lift h i t)) (sns3 c 
 (lifts h i t0))) (\lambda (H3: (sn3 d t)).(\lambda (H4: (sns3 d t0)).(conj 
 (sn3 c (lift h i t)) (sns3 c (lifts h i t0)) (sn3_lift d t H3 c h i H) (H0 
 H4)))) H2)))))) ts)))))).
 
-theorem sn3_gen_def:
- \forall (c: C).(\forall (d: C).(\forall (v: T).(\forall (i: nat).((getl i c 
-(CHead d (Bind Abbr) v)) \to ((sn3 c (TLRef i)) \to (sn3 d v))))))
-\def
- \lambda (c: C).(\lambda (d: C).(\lambda (v: T).(\lambda (i: nat).(\lambda 
-(H: (getl i c (CHead d (Bind Abbr) v))).(\lambda (H0: (sn3 c (TLRef 
-i))).(sn3_gen_lift c v (S i) O (sn3_pr3_trans c (TLRef i) H0 (lift (S i) O v) 
-(pr3_pr2 c (TLRef i) (lift (S i) O v) (pr2_delta c d v i H (TLRef i) (TLRef 
-i) (pr0_refl (TLRef i)) (lift (S i) O v) (subst0_lref v i)))) d (getl_drop 
-Abbr c d v i H))))))).
-
-theorem sn3_cdelta:
- \forall (v: T).(\forall (t: T).(\forall (i: nat).(((\forall (w: T).(ex T 
-(\lambda (u: T).(subst0 i w t u))))) \to (\forall (c: C).(\forall (d: 
-C).((getl i c (CHead d (Bind Abbr) v)) \to ((sn3 c t) \to (sn3 d v))))))))
-\def
- \lambda (v: T).(\lambda (t: T).(\lambda (i: nat).(\lambda (H: ((\forall (w: 
-T).(ex T (\lambda (u: T).(subst0 i w t u)))))).(let H_x \def (H v) in (let H0 
-\def H_x in (ex_ind T (\lambda (u: T).(subst0 i v t u)) (\forall (c: 
-C).(\forall (d: C).((getl i c (CHead d (Bind Abbr) v)) \to ((sn3 c t) \to 
-(sn3 d v))))) (\lambda (x: T).(\lambda (H1: (subst0 i v t x)).(subst0_ind 
-(\lambda (n: nat).(\lambda (t0: T).(\lambda (t1: T).(\lambda (_: T).(\forall 
-(c: C).(\forall (d: C).((getl n c (CHead d (Bind Abbr) t0)) \to ((sn3 c t1) 
-\to (sn3 d t0))))))))) (\lambda (v0: T).(\lambda (i0: nat).(\lambda (c: 
-C).(\lambda (d: C).(\lambda (H2: (getl i0 c (CHead d (Bind Abbr) 
-v0))).(\lambda (H3: (sn3 c (TLRef i0))).(sn3_gen_def c d v0 i0 H2 H3))))))) 
-(\lambda (v0: T).(\lambda (u2: T).(\lambda (u1: T).(\lambda (i0: 
-nat).(\lambda (_: (subst0 i0 v0 u1 u2)).(\lambda (H3: ((\forall (c: 
-C).(\forall (d: C).((getl i0 c (CHead d (Bind Abbr) v0)) \to ((sn3 c u1) \to 
-(sn3 d v0))))))).(\lambda (t0: T).(\lambda (k: K).(\lambda (c: C).(\lambda 
-(d: C).(\lambda (H4: (getl i0 c (CHead d (Bind Abbr) v0))).(\lambda (H5: (sn3 
-c (THead k u1 t0))).(let H_y \def (sn3_gen_head k c u1 t0 H5) in (H3 c d H4 
-H_y)))))))))))))) (\lambda (k: K).(\lambda (v0: T).(\lambda (t2: T).(\lambda 
-(t1: T).(\lambda (i0: nat).(\lambda (H2: (subst0 (s k i0) v0 t1 t2)).(\lambda 
-(H3: ((\forall (c: C).(\forall (d: C).((getl (s k i0) c (CHead d (Bind Abbr) 
-v0)) \to ((sn3 c t1) \to (sn3 d v0))))))).(\lambda (u: T).(\lambda (c: 
-C).(\lambda (d: C).(\lambda (H4: (getl i0 c (CHead d (Bind Abbr) 
-v0))).(\lambda (H5: (sn3 c (THead k u t1))).(K_ind (\lambda (k0: K).((subst0 
-(s k0 i0) v0 t1 t2) \to (((\forall (c0: C).(\forall (d0: C).((getl (s k0 i0) 
-c0 (CHead d0 (Bind Abbr) v0)) \to ((sn3 c0 t1) \to (sn3 d0 v0)))))) \to ((sn3 
-c (THead k0 u t1)) \to (sn3 d v0))))) (\lambda (b: B).(\lambda (_: (subst0 (s 
-(Bind b) i0) v0 t1 t2)).(\lambda (H7: ((\forall (c0: C).(\forall (d0: 
-C).((getl (s (Bind b) i0) c0 (CHead d0 (Bind Abbr) v0)) \to ((sn3 c0 t1) \to 
-(sn3 d0 v0))))))).(\lambda (H8: (sn3 c (THead (Bind b) u t1))).(let H_x0 \def 
-(sn3_gen_bind b c u t1 H8) in (let H9 \def H_x0 in (and_ind (sn3 c u) (sn3 
-(CHead c (Bind b) u) t1) (sn3 d v0) (\lambda (_: (sn3 c u)).(\lambda (H11: 
-(sn3 (CHead c (Bind b) u) t1)).(H7 (CHead c (Bind b) u) d (getl_clear_bind b 
-(CHead c (Bind b) u) c u (clear_bind b c u) (CHead d (Bind Abbr) v0) i0 H4) 
-H11))) H9))))))) (\lambda (f: F).(\lambda (_: (subst0 (s (Flat f) i0) v0 t1 
-t2)).(\lambda (H7: ((\forall (c0: C).(\forall (d0: C).((getl (s (Flat f) i0) 
-c0 (CHead d0 (Bind Abbr) v0)) \to ((sn3 c0 t1) \to (sn3 d0 v0))))))).(\lambda 
-(H8: (sn3 c (THead (Flat f) u t1))).(let H_x0 \def (sn3_gen_flat f c u t1 H8) 
-in (let H9 \def H_x0 in (and_ind (sn3 c u) (sn3 c t1) (sn3 d v0) (\lambda (_: 
-(sn3 c u)).(\lambda (H11: (sn3 c t1)).(H7 c d H4 H11))) H9))))))) k H2 H3 
-H5))))))))))))) (\lambda (v0: T).(\lambda (u1: T).(\lambda (u2: T).(\lambda 
-(i0: nat).(\lambda (_: (subst0 i0 v0 u1 u2)).(\lambda (H3: ((\forall (c: 
-C).(\forall (d: C).((getl i0 c (CHead d (Bind Abbr) v0)) \to ((sn3 c u1) \to 
-(sn3 d v0))))))).(\lambda (k: K).(\lambda (t1: T).(\lambda (t2: T).(\lambda 
-(_: (subst0 (s k i0) v0 t1 t2)).(\lambda (_: ((\forall (c: C).(\forall (d: 
-C).((getl (s k i0) c (CHead d (Bind Abbr) v0)) \to ((sn3 c t1) \to (sn3 d 
-v0))))))).(\lambda (c: C).(\lambda (d: C).(\lambda (H6: (getl i0 c (CHead d 
-(Bind Abbr) v0))).(\lambda (H7: (sn3 c (THead k u1 t1))).(let H_y \def 
-(sn3_gen_head k c u1 t1 H7) in (H3 c d H6 H_y))))))))))))))))) i v t x H1))) 
-H0)))))).
-