\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))))))).
(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
+(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)
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
+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
\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
(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
(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:
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
(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)))).
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
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)))))).