(* This file was automatically generated: do not edit *********************)
-include "Basic-1/ex2/defs.ma".
+include "basic_1/ex2/defs.ma".
-include "Basic-1/nf2/defs.ma".
+include "basic_1/nf2/defs.ma".
-include "Basic-1/pr2/fwd.ma".
+include "basic_1/pr2/fwd.ma".
-include "Basic-1/arity/fwd.ma".
+include "basic_1/arity/fwd.ma".
-theorem ex2_nf2:
+lemma ex2_nf2:
nf2 ex2_c ex2_t
\def
\lambda (t2: T).(\lambda (H: (pr2 (CSort O) (THead (Flat Appl) (TSort O)
(eq_ind T x2 (\lambda (t: T).(eq T t2 (THead (Bind Abbr) t x3))) H3 (TSort O)
(pr2_gen_sort (CSort O) x2 O H4)) in (eq_ind_r T (THead (Bind Abbr) (TSort O)
x3) (\lambda (t: T).(eq T (THead (Flat Appl) (TSort O) (TSort O)) t)) (let H7
-\def (eq_ind T (TSort O) (\lambda (ee: T).(match ee in T return (\lambda (_:
-T).Prop) with [(TSort _) \Rightarrow True | (TLRef _) \Rightarrow False |
-(THead _ _ _) \Rightarrow False])) I (THead (Bind Abst) x0 x1) H2) in
-(False_ind (eq T (THead (Flat Appl) (TSort O) (TSort O)) (THead (Bind Abbr)
-(TSort O) x3)) H7)) t2 H6)))))))))) H1)) (\lambda (H1: (ex6_6 B T T T T T
-(\lambda (b: B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_:
-T).(\lambda (_: T).(not (eq B b Abst)))))))) (\lambda (b: B).(\lambda (y1:
-T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(eq T
-(TSort O) (THead (Bind b) y1 z1)))))))) (\lambda (b: B).(\lambda (_:
-T).(\lambda (_: T).(\lambda (z2: T).(\lambda (u2: T).(\lambda (y2: T).(eq T
-t2 (THead (Bind b) y2 (THead (Flat Appl) (lift (S O) O u2) z2)))))))))
-(\lambda (_: B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (u2:
-T).(\lambda (_: T).(pr2 (CSort O) (TSort O) u2))))))) (\lambda (_:
-B).(\lambda (y1: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda
-(y2: T).(pr2 (CSort O) y1 y2))))))) (\lambda (b: B).(\lambda (_: T).(\lambda
-(z1: T).(\lambda (z2: T).(\lambda (_: T).(\lambda (y2: T).(pr2 (CHead (CSort
-O) (Bind b) y2) z1 z2))))))))).(ex6_6_ind B T T T T T (\lambda (b:
-B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda
-(_: T).(not (eq B b Abst)))))))) (\lambda (b: B).(\lambda (y1: T).(\lambda
-(z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(eq T (TSort O)
-(THead (Bind b) y1 z1)))))))) (\lambda (b: B).(\lambda (_: T).(\lambda (_:
+\def (eq_ind T (TSort O) (\lambda (ee: T).(match ee with [(TSort _)
+\Rightarrow True | (TLRef _) \Rightarrow False | (THead _ _ _) \Rightarrow
+False])) I (THead (Bind Abst) x0 x1) H2) in (False_ind (eq T (THead (Flat
+Appl) (TSort O) (TSort O)) (THead (Bind Abbr) (TSort O) x3)) H7)) t2
+H6)))))))))) H1)) (\lambda (H1: (ex6_6 B T T T T T (\lambda (b: B).(\lambda
+(_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(not
+(eq B b Abst)))))))) (\lambda (b: B).(\lambda (y1: T).(\lambda (z1:
+T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(eq T (TSort O) (THead
+(Bind b) y1 z1)))))))) (\lambda (b: B).(\lambda (_: T).(\lambda (_:
+T).(\lambda (z2: T).(\lambda (u2: T).(\lambda (y2: T).(eq T t2 (THead (Bind
+b) y2 (THead (Flat Appl) (lift (S O) O u2) z2))))))))) (\lambda (_:
+B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda
+(_: T).(pr2 (CSort O) (TSort O) u2))))))) (\lambda (_: B).(\lambda (y1:
+T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (y2: T).(pr2
+(CSort O) y1 y2))))))) (\lambda (b: B).(\lambda (_: T).(\lambda (z1:
+T).(\lambda (z2: T).(\lambda (_: T).(\lambda (y2: T).(pr2 (CHead (CSort O)
+(Bind b) y2) z1 z2))))))))).(ex6_6_ind B T T T T T (\lambda (b: B).(\lambda
+(_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(not
+(eq B b Abst)))))))) (\lambda (b: B).(\lambda (y1: T).(\lambda (z1:
+T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(eq T (TSort O) (THead
+(Bind b) y1 z1)))))))) (\lambda (b: B).(\lambda (_: T).(\lambda (_:
T).(\lambda (z2: T).(\lambda (u2: T).(\lambda (y2: T).(eq T t2 (THead (Bind
b) y2 (THead (Flat Appl) (lift (S O) O u2) z2))))))))) (\lambda (_:
B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda
(Flat Appl) (lift (S O) O t) x3)))) H4 (TSort O) (pr2_gen_sort (CSort O) x4 O
H5)) in (eq_ind_r T (THead (Bind x0) x5 (THead (Flat Appl) (lift (S O) O
(TSort O)) x3)) (\lambda (t: T).(eq T (THead (Flat Appl) (TSort O) (TSort O))
-t)) (let H9 \def (eq_ind T (TSort O) (\lambda (ee: T).(match ee in T return
-(\lambda (_: T).Prop) with [(TSort _) \Rightarrow True | (TLRef _)
-\Rightarrow False | (THead _ _ _) \Rightarrow False])) I (THead (Bind x0) x1
-x2) H3) in (False_ind (eq T (THead (Flat Appl) (TSort O) (TSort O)) (THead
-(Bind x0) x5 (THead (Flat Appl) (lift (S O) O (TSort O)) x3))) H9)) t2
-H8))))))))))))))) H1)) H0))).
-(* COMMENTS
-Initial nodes: 1939
-END *)
+t)) (let H9 \def (eq_ind T (TSort O) (\lambda (ee: T).(match ee with [(TSort
+_) \Rightarrow True | (TLRef _) \Rightarrow False | (THead _ _ _) \Rightarrow
+False])) I (THead (Bind x0) x1 x2) H3) in (False_ind (eq T (THead (Flat Appl)
+(TSort O) (TSort O)) (THead (Bind x0) x5 (THead (Flat Appl) (lift (S O) O
+(TSort O)) x3))) H9)) t2 H8))))))))))))))) H1)) H0))).
-theorem ex2_arity:
+lemma ex2_arity:
\forall (g: G).(\forall (a: A).((arity g ex2_c ex2_t a) \to (\forall (P:
Prop).P)))
\def
a4))) (\lambda (a3: A).(\lambda (a4: A).(eq A (ASort O O) (AHead a3 a4)))) P
(\lambda (x0: A).(\lambda (x1: A).(\lambda (_: (leq g x x0)).(\lambda (_:
(leq g a x1)).(\lambda (H6: (eq A (ASort O O) (AHead x0 x1))).(let H7 \def
-(eq_ind A (ASort O O) (\lambda (ee: A).(match ee in A return (\lambda (_:
-A).Prop) with [(ASort _ _) \Rightarrow True | (AHead _ _) \Rightarrow
-False])) I (AHead x0 x1) H6) in (False_ind P H7))))))) H3)))))) H0))))).
-(* COMMENTS
-Initial nodes: 289
-END *)
+(eq_ind A (ASort O O) (\lambda (ee: A).(match ee with [(ASort _ _)
+\Rightarrow True | (AHead _ _) \Rightarrow False])) I (AHead x0 x1) H6) in
+(False_ind P H7))))))) H3)))))) H0))))).