include "basic_1/pr3/iso.ma".
-theorem sn3_pr3_trans:
+lemma sn3_pr3_trans:
\forall (c: C).(\forall (t1: T).((sn3 c t1) \to (\forall (t2: T).((pr3 c t1
t2) \to (sn3 c t2)))))
\def
H6) in (H0 t0 H8 H7))))) (\lambda (H6: (((eq T t2 t3) \to (\forall (P:
Prop).P)))).(H1 t3 H6 H2 t0 H4)) H5)))))))))))) t1 H))).
-theorem sn3_pr2_intro:
+lemma sn3_pr2_intro:
\forall (c: C).(\forall (t1: T).(((\forall (t2: T).((((eq T t1 t2) \to
(\forall (P: Prop).P))) \to ((pr2 c t1 t2) \to (sn3 c t2))))) \to (sn3 c t1)))
\def
t2)).(sn3_pr3_trans c t0 (sn3_sing c t0 H3) t2 (pr3_pr2 c t0 t2 H8)))
H7))))))))) t H2)))))) u H))).
-theorem sn3_cflat:
+lemma sn3_cflat:
\forall (c: C).(\forall (t: T).((sn3 c t) \to (\forall (f: F).(\forall (u:
T).(sn3 (CHead c (Flat f) u) t)))))
\def
Prop).P)))).(\lambda (H3: (pr2 (CHead c (Flat f) u) t1 t2)).(H1 t2 H2
(pr3_pr2 c t1 t2 (pr2_gen_cflat f c u t1 t2 H3)))))))))) t H))))).
-theorem sn3_shift:
+lemma sn3_shift:
\forall (b: B).(\forall (c: C).(\forall (v: T).(\forall (t: T).((sn3 c
(THead (Bind b) v t)) \to (sn3 (CHead c (Bind b) v) t)))))
\def
(Bind b) v) t) (\lambda (_: (sn3 c v)).(\lambda (H2: (sn3 (CHead c (Bind b)
v) t)).H2)) H0))))))).
-theorem sn3_change:
+lemma sn3_change:
\forall (b: B).((not (eq B b Abbr)) \to (\forall (c: C).(\forall (v1:
T).(\forall (t: T).((sn3 (CHead c (Bind b) v1) t) \to (\forall (v2: T).(sn3
(CHead c (Bind b) v2) t)))))))
(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:
+lemma 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
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:
+lemma 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))))))))
(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:
+lemma 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)
t)))))))
False with []) in H29) x1 H24)))))))) H21)) H20)) t3 H15)))))))))))))) H12))
H11))))))))) w H4))))))))))) y H0))))) H)))).
-theorem sn3_appl_lref:
+lemma sn3_appl_lref:
\forall (c: C).(\forall (i: nat).((nf2 c (TLRef i)) \to (\forall (v:
T).((sn3 c v) \to (sn3 c (THead (Flat Appl) v (TLRef i)))))))
\def
(False_ind (sn3 c (THead (Bind x0) x5 (THead (Flat Appl) (lift (S O) O x4)
x3))) H14)) t2 H9)))))))))))))) H6)) H5))))))))) v H0))))).
-theorem sn3_appl_abbr:
+lemma sn3_appl_abbr:
\forall (c: C).(\forall (d: C).(\forall (w: T).(\forall (i: nat).((getl i c
(CHead d (Bind Abbr) w)) \to (\forall (v: T).((sn3 c (THead (Flat Appl) v
(lift (S i) O w))) \to (sn3 c (THead (Flat Appl) v (TLRef i)))))))))
Appl) v2 u2))))))).(sn3_appl_appl v1 (THeads (Flat Appl) vs t1) c H v2 H0
H1))))))))).
-theorem sn3_appls_lref:
+lemma sn3_appls_lref:
\forall (c: C).(\forall (i: nat).((nf2 c (TLRef i)) \to (\forall (us:
TList).((sns3 c us) \to (sn3 c (THeads (Flat Appl) us (TLRef i)))))))
\def
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)))).
-theorem sn3_lift:
+lemma sn3_lift:
\forall (d: C).(\forall (t: T).((sn3 d t) \to (\forall (c: C).(\forall (h:
nat).(\forall (i: nat).((drop h i c d) \to (sn3 c (lift h i t))))))))
\def
(refl_equal T (lift h i t1)) P))))) (pr3_pr2 d t1 x H7) c h i H2) t2 H6)))))
H5))))))))))))) t H))).
-theorem sn3_abbr:
+lemma sn3_abbr:
\forall (c: C).(\forall (d: C).(\forall (v: T).(\forall (i: nat).((getl i c
(CHead d (Bind Abbr) v)) \to ((sn3 d v) \to (sn3 c (TLRef i)))))))
\def
v))) H12 d H11) in (sn3_lift d v H0 c (S i) O (getl_drop Abbr c d v i H13)))
x1 H10)))) H9))) t2 H6)))))) H4)) H3))))))))))).
-theorem sn3_appls_abbr:
+lemma sn3_appls_abbr:
\forall (c: C).(\forall (d: C).(\forall (w: T).(\forall (i: nat).((getl i c
(CHead d (Bind Abbr) w)) \to (\forall (vs: TList).((sn3 c (THeads (Flat Appl)
vs (lift (S i) O w))) \to (sn3 c (THeads (Flat Appl) vs (TLRef i)))))))))
(pr3_iso_appls_abbr c d w i H (TCons t t0) u2 H6 H7) v Appl))))))))
H3)))))))) vs0))) vs)))))).
-theorem sns3_lifts:
+lemma sns3_lifts:
\forall (c: C).(\forall (d: C).(\forall (h: nat).(\forall (i: nat).((drop h
i c d) \to (\forall (ts: TList).((sns3 d ts) \to (sns3 c (lifts h i ts))))))))
\def