include "basic_1/getl/drop.ma".
-theorem pr2_ind:
+implied lemma pr2_ind:
\forall (P: ((C \to (T \to (T \to Prop))))).(((\forall (c: C).(\forall (t1:
T).(\forall (t2: T).((pr0 t1 t2) \to (P c t1 t2)))))) \to (((\forall (c:
C).(\forall (d: C).(\forall (u: T).(\forall (i: nat).((getl i c (CHead d
\Rightarrow (f x x0 x1 x2) | (pr2_delta x x0 x1 x2 x3 x4 x5 x6 x7 x8)
\Rightarrow (f0 x x0 x1 x2 x3 x4 x5 x6 x7 x8)]))))))).
-theorem pr2_gen_sort:
+lemma pr2_gen_sort:
\forall (c: C).(\forall (x: T).(\forall (n: nat).((pr2 c (TSort n) x) \to
(eq T x (TSort n)))))
\def
(pr0_gen_sort t2 n H5)) in (subst0_gen_sort u t i n H6 (eq T t (TSort n))))
t1 H4))))))))))))) c y x H0))) H)))).
-theorem pr2_gen_lref:
+lemma pr2_gen_lref:
\forall (c: C).(\forall (x: T).(\forall (n: nat).((pr2 c (TLRef n) x) \to
(or (eq T x (TLRef n)) (ex2_2 C T (\lambda (d: C).(\lambda (u: T).(getl n c
(CHead d (Bind Abbr) u)))) (\lambda (_: C).(\lambda (u: T).(eq T x (lift (S
n) O u0)))) d u H9 (refl_equal T (lift (S n) O u))))) t H8)))
(subst0_gen_lref u t i n H6))) t1 H4))))))))))))) c y x H0))) H)))).
-theorem pr2_gen_abst:
+lemma pr2_gen_abst:
\forall (c: C).(\forall (u1: T).(\forall (t1: T).(\forall (x: T).((pr2 c
(THead (Bind Abst) u1 t1) x) \to (ex3_2 T T (\lambda (u2: T).(\lambda (t2:
T).(eq T x (THead (Bind Abst) u2 t2)))) (\lambda (u2: T).(\lambda (_: T).(pr2
H13)))) t H11)))))) H10)) (subst0_gen_head (Bind Abst) u x0 x1 t i H9))))))))
(pr0_gen_abst u1 t1 t2 H5)))))))))))))) c y x H0))) H))))).
-theorem pr2_gen_cast:
+lemma pr2_gen_cast:
\forall (c: C).(\forall (u1: T).(\forall (t1: T).(\forall (x: T).((pr2 c
(THead (Flat Cast) u1 t1) x) \to (or (ex3_2 T T (\lambda (u2: T).(\lambda
(t2: T).(eq T x (THead (Flat Cast) u2 t2)))) (\lambda (u2: T).(\lambda (_:
(pr2_delta c0 d u i H1 t1 t2 H6 t H3))) (pr0_gen_cast u1 t1 t2
H5)))))))))))))) c y x H0))) H))))).
-theorem pr2_gen_csort:
+lemma pr2_gen_csort:
\forall (t1: T).(\forall (t2: T).(\forall (n: nat).((pr2 (CSort n) t1 t2)
\to (pr0 t1 t2))))
\def
(Bind Abbr) u))) H1 (CSort n) H4) in (getl_gen_sort n i (CHead d (Bind Abbr)
u) H5 (pr0 t3 t)))))))))))))) y t1 t2 H0))) H)))).
-theorem pr2_gen_appl:
+lemma pr2_gen_appl:
\forall (c: C).(\forall (u1: T).(\forall (t1: T).(\forall (x: T).((pr2 c
(THead (Flat Appl) u1 t1) x) \to (or3 (ex3_2 T T (\lambda (u2: T).(\lambda
(t2: T).(eq T x (THead (Flat Appl) u2 t2)))) (\lambda (u2: T).(\lambda (_:
(Flat Appl) (lift (S O) O x3) x5) t i H13)) t1 H8)))))))))))))) H6))
(pr0_gen_appl u1 t1 t2 H5)))))))))))))) c y x H0))) H))))).
-theorem pr2_gen_lift:
+lemma pr2_gen_lift:
\forall (c: C).(\forall (t1: T).(\forall (x: T).(\forall (h: nat).(\forall
(d: nat).((pr2 c (lift h d t1) x) \to (\forall (e: C).((drop h d c e) \to
(ex2 T (\lambda (t2: T).(eq T x (lift h d t2))) (\lambda (t2: T).(pr2 e t1