X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_1%2Fpc3%2Ffwd.ma;h=99239c2a7781579c017e9bd9496c3e1882f00627;hb=57ae1762497a5f3ea75740e2908e04adb8642cc2;hp=c89e4563c37b4ac1e52aaa5f5b9b65f08a794431;hpb=88a68a9c334646bc17314d5327cd3b790202acd6;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_1/pc3/fwd.ma b/matita/matita/contribs/lambdadelta/basic_1/pc3/fwd.ma
index c89e4563c..99239c2a7 100644
--- a/matita/matita/contribs/lambdadelta/basic_1/pc3/fwd.ma
+++ b/matita/matita/contribs/lambdadelta/basic_1/pc3/fwd.ma
@@ -14,11 +14,9 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "Basic-1/pc3/props.ma".
+include "basic_1/pc3/props.ma".
 
-include "Basic-1/pr3/fwd.ma".
-
-theorem pc3_gen_sort:
+lemma pc3_gen_sort:
  \forall (c: C).(\forall (m: nat).(\forall (n: nat).((pc3 c (TSort m) (TSort 
 n)) \to (eq nat m n))))
 \def
@@ -28,14 +26,11 @@ n)) \to (eq nat m n))))
 T).(\lambda (H1: (pr3 c (TSort m) x)).(\lambda (H2: (pr3 c (TSort n) x)).(let 
 H3 \def (eq_ind T x (\lambda (t: T).(eq T t (TSort n))) (pr3_gen_sort c x n 
 H2) (TSort m) (pr3_gen_sort c x m H1)) in (let H4 \def (f_equal T nat 
-(\lambda (e: T).(match e in T return (\lambda (_: T).nat) with [(TSort n0) 
-\Rightarrow n0 | (TLRef _) \Rightarrow m | (THead _ _ _) \Rightarrow m])) 
-(TSort m) (TSort n) H3) in H4))))) H0))))).
-(* COMMENTS
-Initial nodes: 153
-END *)
+(\lambda (e: T).(match e with [(TSort n0) \Rightarrow n0 | (TLRef _) 
+\Rightarrow m | (THead _ _ _) \Rightarrow m])) (TSort m) (TSort n) H3) in 
+H4))))) H0))))).
 
-theorem pc3_gen_abst:
+lemma pc3_gen_abst:
  \forall (c: C).(\forall (u1: T).(\forall (u2: T).(\forall (t1: T).(\forall 
 (t2: T).((pc3 c (THead (Bind Abst) u1 t1) (THead (Bind Abst) u2 t2)) \to 
 (land (pc3 c u1 u2) (\forall (b: B).(\forall (u: T).(pc3 (CHead c (Bind b) u) 
@@ -65,23 +60,20 @@ t1 t2)))) (\lambda (x2: T).(\lambda (x3: T).(\lambda (H8: (eq T x (THead
 (b: B).(\forall (u: T).(pr3 (CHead c (Bind b) u) t1 x3))))).(let H11 \def 
 (eq_ind T x (\lambda (t: T).(eq T t (THead (Bind Abst) x0 x1))) H4 (THead 
 (Bind Abst) x2 x3) H8) in (let H12 \def (f_equal T T (\lambda (e: T).(match e 
-in T return (\lambda (_: T).T) with [(TSort _) \Rightarrow x2 | (TLRef _) 
-\Rightarrow x2 | (THead _ t _) \Rightarrow t])) (THead (Bind Abst) x2 x3) 
-(THead (Bind Abst) x0 x1) H11) in ((let H13 \def (f_equal T T (\lambda (e: 
-T).(match e in T return (\lambda (_: T).T) with [(TSort _) \Rightarrow x3 | 
-(TLRef _) \Rightarrow x3 | (THead _ _ t) \Rightarrow t])) (THead (Bind Abst) 
-x2 x3) (THead (Bind Abst) x0 x1) H11) in (\lambda (H14: (eq T x2 x0)).(let 
-H15 \def (eq_ind T x3 (\lambda (t: T).(\forall (b: B).(\forall (u: T).(pr3 
-(CHead c (Bind b) u) t1 t)))) H10 x1 H13) in (let H16 \def (eq_ind T x2 
-(\lambda (t: T).(pr3 c u1 t)) H9 x0 H14) in (conj (pc3 c u1 u2) (\forall (b: 
-B).(\forall (u: T).(pc3 (CHead c (Bind b) u) t1 t2))) (pc3_pr3_t c u1 x0 H16 
-u2 H5) (\lambda (b: B).(\lambda (u: T).(pc3_pr3_t (CHead c (Bind b) u) t1 x1 
-(H15 b u) t2 (H6 b u))))))))) H12)))))))) H7))))))) H3))))) H0))))))).
-(* COMMENTS
-Initial nodes: 715
-END *)
+with [(TSort _) \Rightarrow x2 | (TLRef _) \Rightarrow x2 | (THead _ t _) 
+\Rightarrow t])) (THead (Bind Abst) x2 x3) (THead (Bind Abst) x0 x1) H11) in 
+((let H13 \def (f_equal T T (\lambda (e: T).(match e with [(TSort _) 
+\Rightarrow x3 | (TLRef _) \Rightarrow x3 | (THead _ _ t) \Rightarrow t])) 
+(THead (Bind Abst) x2 x3) (THead (Bind Abst) x0 x1) H11) in (\lambda (H14: 
+(eq T x2 x0)).(let H15 \def (eq_ind T x3 (\lambda (t: T).(\forall (b: 
+B).(\forall (u: T).(pr3 (CHead c (Bind b) u) t1 t)))) H10 x1 H13) in (let H16 
+\def (eq_ind T x2 (\lambda (t: T).(pr3 c u1 t)) H9 x0 H14) in (conj (pc3 c u1 
+u2) (\forall (b: B).(\forall (u: T).(pc3 (CHead c (Bind b) u) t1 t2))) 
+(pc3_pr3_t c u1 x0 H16 u2 H5) (\lambda (b: B).(\lambda (u: T).(pc3_pr3_t 
+(CHead c (Bind b) u) t1 x1 (H15 b u) t2 (H6 b u))))))))) H12)))))))) 
+H7))))))) H3))))) H0))))))).
 
-theorem pc3_gen_abst_shift:
+lemma pc3_gen_abst_shift:
  \forall (c: C).(\forall (u: T).(\forall (t1: T).(\forall (t2: T).((pc3 c 
 (THead (Bind Abst) u t1) (THead (Bind Abst) u t2)) \to (pc3 (CHead c (Bind 
 Abst) u) t1 t2)))))
@@ -93,11 +85,8 @@ Abst) u) t1 t2)))))
 (CHead c (Bind Abst) u) t1 t2) (\lambda (_: (pc3 c u u)).(\lambda (H2: 
 ((\forall (b: B).(\forall (u0: T).(pc3 (CHead c (Bind b) u0) t1 t2))))).(H2 
 Abst u))) H0))))))).
-(* COMMENTS
-Initial nodes: 129
-END *)
 
-theorem pc3_gen_lift:
+lemma pc3_gen_lift:
  \forall (c: C).(\forall (t1: T).(\forall (t2: T).(\forall (h: nat).(\forall 
 (d: nat).((pc3 c (lift h d t1) (lift h d t2)) \to (\forall (e: C).((drop h d 
 c e) \to (pc3 e t1 t2))))))))
@@ -117,11 +106,8 @@ h d x1))).(\lambda (H9: (pr3 e t1 x1)).(let H10 \def (eq_ind T x (\lambda (t:
 T).(eq T t (lift h d x0))) H5 (lift h d x1) H8) in (let H11 \def (eq_ind T x1 
 (\lambda (t: T).(pr3 e t1 t)) H9 x0 (lift_inj x1 x0 h d H10)) in (pc3_pr3_t e 
 t1 x0 H11 t2 H6)))))) H7))))) H4))))) H1))))))))).
-(* COMMENTS
-Initial nodes: 363
-END *)
 
-theorem pc3_gen_not_abst:
+lemma pc3_gen_not_abst:
  \forall (b: B).((not (eq B b Abst)) \to (\forall (c: C).(\forall (t1: 
 T).(\forall (t2: T).(\forall (u1: T).(\forall (u2: T).((pc3 c (THead (Bind b) 
 u1 t1) (THead (Bind Abst) u2 t2)) \to (pc3 (CHead c (Bind b) u1) t1 (lift (S 
@@ -161,40 +147,37 @@ T).(\lambda (H10: (eq T x (THead (Bind Abst) x2 x3))).(\lambda (_: (pr3 c u2
 x2)).(\lambda (_: ((\forall (b0: B).(\forall (u: T).(pr3 (CHead c (Bind b0) 
 u) t2 x3))))).(let H13 \def (eq_ind T x (\lambda (t: T).(eq T t (THead (Bind 
 Abbr) x0 x1))) H6 (THead (Bind Abst) x2 x3) H10) in (let H14 \def (eq_ind T 
-(THead (Bind Abst) x2 x3) (\lambda (ee: T).(match ee in T return (\lambda (_: 
-T).Prop) with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow False | 
-(THead k _ _) \Rightarrow (match k in K return (\lambda (_: K).Prop) with 
-[(Bind b0) \Rightarrow (match b0 in B return (\lambda (_: B).Prop) with [Abbr 
-\Rightarrow False | Abst \Rightarrow True | Void \Rightarrow False]) | (Flat 
-_) \Rightarrow False])])) I (THead (Bind Abbr) x0 x1) H13) in (False_ind (pc3 
-(CHead c (Bind Abbr) u1) t1 (lift (S O) O (THead (Bind Abst) u2 t2))) 
-H14)))))))) H9))))))) H5)) (\lambda (H5: (pr3 (CHead c (Bind Abbr) u1) t1 
-(lift (S O) O x))).(let H6 \def (pr3_gen_abst c u2 t2 x H3) in (ex3_2_ind T T 
-(\lambda (u3: T).(\lambda (t3: T).(eq T x (THead (Bind Abst) u3 t3)))) 
-(\lambda (u3: T).(\lambda (_: T).(pr3 c u2 u3))) (\lambda (_: T).(\lambda 
-(t3: T).(\forall (b0: B).(\forall (u: T).(pr3 (CHead c (Bind b0) u) t2 
-t3))))) (pc3 (CHead c (Bind Abbr) u1) t1 (lift (S O) O (THead (Bind Abst) u2 
-t2))) (\lambda (x0: T).(\lambda (x1: T).(\lambda (H7: (eq T x (THead (Bind 
-Abst) x0 x1))).(\lambda (H8: (pr3 c u2 x0)).(\lambda (H9: ((\forall (b0: 
-B).(\forall (u: T).(pr3 (CHead c (Bind b0) u) t2 x1))))).(let H10 \def 
-(eq_ind T x (\lambda (t: T).(pr3 (CHead c (Bind Abbr) u1) t1 (lift (S O) O 
-t))) H5 (THead (Bind Abst) x0 x1) H7) in (pc3_pr3_t (CHead c (Bind Abbr) u1) 
-t1 (lift (S O) O (THead (Bind Abst) x0 x1)) H10 (lift (S O) O (THead (Bind 
-Abst) u2 t2)) (pr3_lift (CHead c (Bind Abbr) u1) c (S O) O (drop_drop (Bind 
-Abbr) O c c (drop_refl c) u1) (THead (Bind Abst) u2 t2) (THead (Bind Abst) x0 
-x1) (pr3_head_12 c u2 x0 H8 (Bind Abst) t2 x1 (H9 Abst x0)))))))))) H6))) 
-H4))))) H1))))))))) (\lambda (H: (not (eq B Abst Abst))).(\lambda (c: 
-C).(\lambda (t1: T).(\lambda (t2: T).(\lambda (u1: T).(\lambda (u2: 
-T).(\lambda (_: (pc3 c (THead (Bind Abst) u1 t1) (THead (Bind Abst) u2 
-t2))).(let H1 \def (match (H (refl_equal B Abst)) in False return (\lambda 
-(_: False).(pc3 (CHead c (Bind Abst) u1) t1 (lift (S O) O (THead (Bind Abst) 
-u2 t2)))) with []) in H1)))))))) (\lambda (_: (not (eq B Void 
-Abst))).(\lambda (c: C).(\lambda (t1: T).(\lambda (t2: T).(\lambda (u1: 
-T).(\lambda (u2: T).(\lambda (H0: (pc3 c (THead (Bind Void) u1 t1) (THead 
-(Bind Abst) u2 t2))).(let H1 \def H0 in (ex2_ind T (\lambda (t: T).(pr3 c 
-(THead (Bind Void) u1 t1) t)) (\lambda (t: T).(pr3 c (THead (Bind Abst) u2 
-t2) t)) (pc3 (CHead c (Bind Void) u1) t1 (lift (S O) O (THead (Bind Abst) u2 
-t2))) (\lambda (x: T).(\lambda (H2: (pr3 c (THead (Bind Void) u1 t1) 
+(THead (Bind Abst) x2 x3) (\lambda (ee: T).(match ee with [(TSort _) 
+\Rightarrow False | (TLRef _) \Rightarrow False | (THead k _ _) \Rightarrow 
+(match k with [(Bind b0) \Rightarrow (match b0 with [Abbr \Rightarrow False | 
+Abst \Rightarrow True | Void \Rightarrow False]) | (Flat _) \Rightarrow 
+False])])) I (THead (Bind Abbr) x0 x1) H13) in (False_ind (pc3 (CHead c (Bind 
+Abbr) u1) t1 (lift (S O) O (THead (Bind Abst) u2 t2))) H14)))))))) H9))))))) 
+H5)) (\lambda (H5: (pr3 (CHead c (Bind Abbr) u1) t1 (lift (S O) O x))).(let 
+H6 \def (pr3_gen_abst c u2 t2 x H3) in (ex3_2_ind T T (\lambda (u3: 
+T).(\lambda (t3: T).(eq T x (THead (Bind Abst) u3 t3)))) (\lambda (u3: 
+T).(\lambda (_: T).(pr3 c u2 u3))) (\lambda (_: T).(\lambda (t3: T).(\forall 
+(b0: B).(\forall (u: T).(pr3 (CHead c (Bind b0) u) t2 t3))))) (pc3 (CHead c 
+(Bind Abbr) u1) t1 (lift (S O) O (THead (Bind Abst) u2 t2))) (\lambda (x0: 
+T).(\lambda (x1: T).(\lambda (H7: (eq T x (THead (Bind Abst) x0 
+x1))).(\lambda (H8: (pr3 c u2 x0)).(\lambda (H9: ((\forall (b0: B).(\forall 
+(u: T).(pr3 (CHead c (Bind b0) u) t2 x1))))).(let H10 \def (eq_ind T x 
+(\lambda (t: T).(pr3 (CHead c (Bind Abbr) u1) t1 (lift (S O) O t))) H5 (THead 
+(Bind Abst) x0 x1) H7) in (pc3_pr3_t (CHead c (Bind Abbr) u1) t1 (lift (S O) 
+O (THead (Bind Abst) x0 x1)) H10 (lift (S O) O (THead (Bind Abst) u2 t2)) 
+(pr3_lift (CHead c (Bind Abbr) u1) c (S O) O (drop_drop (Bind Abbr) O c c 
+(drop_refl c) u1) (THead (Bind Abst) u2 t2) (THead (Bind Abst) x0 x1) 
+(pr3_head_12 c u2 x0 H8 (Bind Abst) t2 x1 (H9 Abst x0)))))))))) H6))) H4))))) 
+H1))))))))) (\lambda (H: (not (eq B Abst Abst))).(\lambda (c: C).(\lambda 
+(t1: T).(\lambda (t2: T).(\lambda (u1: T).(\lambda (u2: T).(\lambda (_: (pc3 
+c (THead (Bind Abst) u1 t1) (THead (Bind Abst) u2 t2))).(let H1 \def (match 
+(H (refl_equal B Abst)) in False with []) in H1)))))))) (\lambda (_: (not (eq 
+B Void Abst))).(\lambda (c: C).(\lambda (t1: T).(\lambda (t2: T).(\lambda 
+(u1: T).(\lambda (u2: T).(\lambda (H0: (pc3 c (THead (Bind Void) u1 t1) 
+(THead (Bind Abst) u2 t2))).(let H1 \def H0 in (ex2_ind T (\lambda (t: 
+T).(pr3 c (THead (Bind Void) u1 t1) t)) (\lambda (t: T).(pr3 c (THead (Bind 
+Abst) u2 t2) t)) (pc3 (CHead c (Bind Void) u1) t1 (lift (S O) O (THead (Bind 
+Abst) u2 t2))) (\lambda (x: T).(\lambda (H2: (pr3 c (THead (Bind Void) u1 t1) 
 x)).(\lambda (H3: (pr3 c (THead (Bind Abst) u2 t2) x)).(let H4 \def 
 (pr3_gen_void c u1 t1 x H2) in (or_ind (ex3_2 T T (\lambda (u3: T).(\lambda 
 (t3: T).(eq T x (THead (Bind Void) u3 t3)))) (\lambda (u3: T).(\lambda (_: 
@@ -221,34 +204,29 @@ Abst) u2 t2))) (\lambda (x2: T).(\lambda (x3: T).(\lambda (H10: (eq T x
 ((\forall (b0: B).(\forall (u: T).(pr3 (CHead c (Bind b0) u) t2 x3))))).(let 
 H13 \def (eq_ind T x (\lambda (t: T).(eq T t (THead (Bind Void) x0 x1))) H6 
 (THead (Bind Abst) x2 x3) H10) in (let H14 \def (eq_ind T (THead (Bind Abst) 
-x2 x3) (\lambda (ee: T).(match ee in T return (\lambda (_: T).Prop) with 
-[(TSort _) \Rightarrow False | (TLRef _) \Rightarrow False | (THead k _ _) 
-\Rightarrow (match k in K return (\lambda (_: K).Prop) with [(Bind b0) 
-\Rightarrow (match b0 in B return (\lambda (_: B).Prop) with [Abbr 
-\Rightarrow False | Abst \Rightarrow True | Void \Rightarrow False]) | (Flat 
-_) \Rightarrow False])])) I (THead (Bind Void) x0 x1) H13) in (False_ind (pc3 
-(CHead c (Bind Void) u1) t1 (lift (S O) O (THead (Bind Abst) u2 t2))) 
-H14)))))))) H9))))))) H5)) (\lambda (H5: (pr3 (CHead c (Bind Void) u1) t1 
-(lift (S O) O x))).(let H6 \def (pr3_gen_abst c u2 t2 x H3) in (ex3_2_ind T T 
-(\lambda (u3: T).(\lambda (t3: T).(eq T x (THead (Bind Abst) u3 t3)))) 
-(\lambda (u3: T).(\lambda (_: T).(pr3 c u2 u3))) (\lambda (_: T).(\lambda 
-(t3: T).(\forall (b0: B).(\forall (u: T).(pr3 (CHead c (Bind b0) u) t2 
-t3))))) (pc3 (CHead c (Bind Void) u1) t1 (lift (S O) O (THead (Bind Abst) u2 
-t2))) (\lambda (x0: T).(\lambda (x1: T).(\lambda (H7: (eq T x (THead (Bind 
-Abst) x0 x1))).(\lambda (H8: (pr3 c u2 x0)).(\lambda (H9: ((\forall (b0: 
-B).(\forall (u: T).(pr3 (CHead c (Bind b0) u) t2 x1))))).(let H10 \def 
-(eq_ind T x (\lambda (t: T).(pr3 (CHead c (Bind Void) u1) t1 (lift (S O) O 
-t))) H5 (THead (Bind Abst) x0 x1) H7) in (pc3_pr3_t (CHead c (Bind Void) u1) 
-t1 (lift (S O) O (THead (Bind Abst) x0 x1)) H10 (lift (S O) O (THead (Bind 
-Abst) u2 t2)) (pr3_lift (CHead c (Bind Void) u1) c (S O) O (drop_drop (Bind 
-Void) O c c (drop_refl c) u1) (THead (Bind Abst) u2 t2) (THead (Bind Abst) x0 
-x1) (pr3_head_12 c u2 x0 H8 (Bind Abst) t2 x1 (H9 Abst x0)))))))))) H6))) 
-H4))))) H1))))))))) b).
-(* COMMENTS
-Initial nodes: 2427
-END *)
+x2 x3) (\lambda (ee: T).(match ee with [(TSort _) \Rightarrow False | (TLRef 
+_) \Rightarrow False | (THead k _ _) \Rightarrow (match k with [(Bind b0) 
+\Rightarrow (match b0 with [Abbr \Rightarrow False | Abst \Rightarrow True | 
+Void \Rightarrow False]) | (Flat _) \Rightarrow False])])) I (THead (Bind 
+Void) x0 x1) H13) in (False_ind (pc3 (CHead c (Bind Void) u1) t1 (lift (S O) 
+O (THead (Bind Abst) u2 t2))) H14)))))))) H9))))))) H5)) (\lambda (H5: (pr3 
+(CHead c (Bind Void) u1) t1 (lift (S O) O x))).(let H6 \def (pr3_gen_abst c 
+u2 t2 x H3) in (ex3_2_ind T T (\lambda (u3: T).(\lambda (t3: T).(eq T x 
+(THead (Bind Abst) u3 t3)))) (\lambda (u3: T).(\lambda (_: T).(pr3 c u2 u3))) 
+(\lambda (_: T).(\lambda (t3: T).(\forall (b0: B).(\forall (u: T).(pr3 (CHead 
+c (Bind b0) u) t2 t3))))) (pc3 (CHead c (Bind Void) u1) t1 (lift (S O) O 
+(THead (Bind Abst) u2 t2))) (\lambda (x0: T).(\lambda (x1: T).(\lambda (H7: 
+(eq T x (THead (Bind Abst) x0 x1))).(\lambda (H8: (pr3 c u2 x0)).(\lambda 
+(H9: ((\forall (b0: B).(\forall (u: T).(pr3 (CHead c (Bind b0) u) t2 
+x1))))).(let H10 \def (eq_ind T x (\lambda (t: T).(pr3 (CHead c (Bind Void) 
+u1) t1 (lift (S O) O t))) H5 (THead (Bind Abst) x0 x1) H7) in (pc3_pr3_t 
+(CHead c (Bind Void) u1) t1 (lift (S O) O (THead (Bind Abst) x0 x1)) H10 
+(lift (S O) O (THead (Bind Abst) u2 t2)) (pr3_lift (CHead c (Bind Void) u1) c 
+(S O) O (drop_drop (Bind Void) O c c (drop_refl c) u1) (THead (Bind Abst) u2 
+t2) (THead (Bind Abst) x0 x1) (pr3_head_12 c u2 x0 H8 (Bind Abst) t2 x1 (H9 
+Abst x0)))))))))) H6))) H4))))) H1))))))))) b).
 
-theorem pc3_gen_lift_abst:
+lemma pc3_gen_lift_abst:
  \forall (c: C).(\forall (t: T).(\forall (t2: T).(\forall (u2: T).(\forall 
 (h: nat).(\forall (d: nat).((pc3 c (lift h d t) (THead (Bind Abst) u2 t2)) 
 \to (\forall (e: C).((drop h d c e) \to (ex3_2 T T (\lambda (u1: T).(\lambda 
@@ -302,11 +280,8 @@ T).(pr3 e t t0)) H6 (THead (Bind Abst) x3 x4) H12) in (ex3_2_intro T T
 T).(\lambda (t1: T).(\forall (b: B).(\forall (u: T).(pr3 (CHead c (Bind b) u) 
 t2 (lift h (S d) t1)))))) x3 x4 H17 H16 H15))))))))) (lift_gen_bind Abst x1 
 x2 x0 h d H11)))))))) H7))))) H4))))) H1)))))))))).
-(* COMMENTS
-Initial nodes: 973
-END *)
 
-theorem pc3_gen_sort_abst:
+lemma pc3_gen_sort_abst:
  \forall (c: C).(\forall (u: T).(\forall (t: T).(\forall (n: nat).((pc3 c 
 (TSort n) (THead (Bind Abst) u t)) \to (\forall (P: Prop).P)))))
 \def
@@ -323,11 +298,7 @@ T).(\lambda (H4: (eq T x (THead (Bind Abst) x0 x1))).(\lambda (_: (pr3 c u
 x0)).(\lambda (_: ((\forall (b: B).(\forall (u0: T).(pr3 (CHead c (Bind b) 
 u0) t x1))))).(let H7 \def (eq_ind T x (\lambda (t0: T).(eq T t0 (TSort n))) 
 (pr3_gen_sort c x n H1) (THead (Bind Abst) x0 x1) H4) in (let H8 \def (eq_ind 
-T (THead (Bind Abst) x0 x1) (\lambda (ee: T).(match ee in T return (\lambda 
-(_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow False 
-| (THead _ _ _) \Rightarrow True])) I (TSort n) H7) in (False_ind P 
-H8)))))))) H3))))) H0))))))).
-(* COMMENTS
-Initial nodes: 303
-END *)
+T (THead (Bind Abst) x0 x1) (\lambda (ee: T).(match ee with [(TSort _) 
+\Rightarrow False | (TLRef _) \Rightarrow False | (THead _ _ _) \Rightarrow 
+True])) I (TSort n) H7) in (False_ind P H8)))))))) H3))))) H0))))))).