(* This file was automatically generated: do not edit *********************)
-include "Basic-1/nf2/defs.ma".
+include "basic_1/nf2/defs.ma".
-include "Basic-1/pr2/clen.ma".
+include "basic_1/pr2/clen.ma".
-include "Basic-1/pr2/fwd.ma".
+include "basic_1/pr0/dec.ma".
-include "Basic-1/pr0/dec.ma".
+include "basic_1/C/props.ma".
-include "Basic-1/C/props.ma".
-
-theorem nf2_dec:
+lemma nf2_dec:
\forall (c: C).(\forall (t1: T).(or (nf2 c t1) (ex2 T (\lambda (t2: T).((eq
T t1 t2) \to (\forall (P: Prop).P))) (\lambda (t2: T).(pr2 c t1 t2)))))
\def
T).(subst0 (clen c0) t t0 t2)) (eq T t1 t2) (\lambda (x0: T).(\lambda (H5:
(eq K (Bind Abst) (Bind Abbr))).(\lambda (_: (pr0 t1 x0)).(\lambda (_:
(subst0 (clen c0) t x0 t2)).(let H8 \def (eq_ind K (Bind Abst) (\lambda (ee:
-K).(match ee 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 (Bind Abbr) H5) in (False_ind (eq T t1 t2) H8)))))) H4)) H3))))))
-(or_introl (\forall (t2: T).((pr2 (CTail (Bind Void) t c0) t1 t2) \to (eq T
-t1 t2))) (ex2 T (\lambda (t2: T).((eq T t1 t2) \to (\forall (P: Prop).P)))
-(\lambda (t2: T).(pr2 (CTail (Bind Void) t c0) t1 t2))) (\lambda (t2:
-T).(\lambda (H2: (pr2 (CTail (Bind Void) t c0) t1 t2)).(let H_x0 \def
+K).(match ee with [(Bind b0) \Rightarrow (match b0 with [Abbr \Rightarrow
+False | Abst \Rightarrow True | Void \Rightarrow False]) | (Flat _)
+\Rightarrow False])) I (Bind Abbr) H5) in (False_ind (eq T t1 t2) H8))))))
+H4)) H3)))))) (or_introl (\forall (t2: T).((pr2 (CTail (Bind Void) t c0) t1
+t2) \to (eq T t1 t2))) (ex2 T (\lambda (t2: T).((eq T t1 t2) \to (\forall (P:
+Prop).P))) (\lambda (t2: T).(pr2 (CTail (Bind Void) t c0) t1 t2))) (\lambda
+(t2: T).(\lambda (H2: (pr2 (CTail (Bind Void) t c0) t1 t2)).(let H_x0 \def
(pr2_gen_ctail (Bind Void) c0 t t1 t2 H2) in (let H3 \def H_x0 in (or_ind
(pr2 c0 t1 t2) (ex3 T (\lambda (_: T).(eq K (Bind Void) (Bind Abbr)))
(\lambda (t0: T).(pr0 t1 t0)) (\lambda (t0: T).(subst0 (clen c0) t t0 t2)))
T).(subst0 (clen c0) t t0 t2)) (eq T t1 t2) (\lambda (x0: T).(\lambda (H5:
(eq K (Bind Void) (Bind Abbr))).(\lambda (_: (pr0 t1 x0)).(\lambda (_:
(subst0 (clen c0) t x0 t2)).(let H8 \def (eq_ind K (Bind Void) (\lambda (ee:
-K).(match ee in K return (\lambda (_: K).Prop) with [(Bind b0) \Rightarrow
-(match b0 in B return (\lambda (_: B).Prop) with [Abbr \Rightarrow False |
-Abst \Rightarrow False | Void \Rightarrow True]) | (Flat _) \Rightarrow
-False])) I (Bind Abbr) H5) in (False_ind (eq T t1 t2) H8)))))) H4)) H3))))))
-b)) (\lambda (f: F).(or_introl (\forall (t2: T).((pr2 (CTail (Flat f) t c0)
-t1 t2) \to (eq T t1 t2))) (ex2 T (\lambda (t2: T).((eq T t1 t2) \to (\forall
-(P: Prop).P))) (\lambda (t2: T).(pr2 (CTail (Flat f) t c0) t1 t2))) (\lambda
-(t2: T).(\lambda (H2: (pr2 (CTail (Flat f) t c0) t1 t2)).(let H_x0 \def
-(pr2_gen_ctail (Flat f) c0 t t1 t2 H2) in (let H3 \def H_x0 in (or_ind (pr2
-c0 t1 t2) (ex3 T (\lambda (_: T).(eq K (Flat f) (Bind Abbr))) (\lambda (t0:
-T).(pr0 t1 t0)) (\lambda (t0: T).(subst0 (clen c0) t t0 t2))) (eq T t1 t2)
-(\lambda (H4: (pr2 c0 t1 t2)).(H1 t2 H4)) (\lambda (H4: (ex3 T (\lambda (_:
+K).(match ee with [(Bind b0) \Rightarrow (match b0 with [Abbr \Rightarrow
+False | Abst \Rightarrow False | Void \Rightarrow True]) | (Flat _)
+\Rightarrow False])) I (Bind Abbr) H5) in (False_ind (eq T t1 t2) H8))))))
+H4)) H3)))))) b)) (\lambda (f: F).(or_introl (\forall (t2: T).((pr2 (CTail
+(Flat f) t c0) t1 t2) \to (eq T t1 t2))) (ex2 T (\lambda (t2: T).((eq T t1
+t2) \to (\forall (P: Prop).P))) (\lambda (t2: T).(pr2 (CTail (Flat f) t c0)
+t1 t2))) (\lambda (t2: T).(\lambda (H2: (pr2 (CTail (Flat f) t c0) t1
+t2)).(let H_x0 \def (pr2_gen_ctail (Flat f) c0 t t1 t2 H2) in (let H3 \def
+H_x0 in (or_ind (pr2 c0 t1 t2) (ex3 T (\lambda (_: T).(eq K (Flat f) (Bind
+Abbr))) (\lambda (t0: T).(pr0 t1 t0)) (\lambda (t0: T).(subst0 (clen c0) t t0
+t2))) (eq T t1 t2) (\lambda (H4: (pr2 c0 t1 t2)).(H1 t2 H4)) (\lambda (H4:
+(ex3 T (\lambda (_: T).(eq K (Flat f) (Bind Abbr))) (\lambda (t0: T).(pr0 t1
+t0)) (\lambda (t0: T).(subst0 (clen c0) t t0 t2)))).(ex3_ind T (\lambda (_:
T).(eq K (Flat f) (Bind Abbr))) (\lambda (t0: T).(pr0 t1 t0)) (\lambda (t0:
-T).(subst0 (clen c0) t t0 t2)))).(ex3_ind T (\lambda (_: T).(eq K (Flat f)
-(Bind Abbr))) (\lambda (t0: T).(pr0 t1 t0)) (\lambda (t0: T).(subst0 (clen
-c0) t t0 t2)) (eq T t1 t2) (\lambda (x0: T).(\lambda (H5: (eq K (Flat f)
-(Bind Abbr))).(\lambda (_: (pr0 t1 x0)).(\lambda (_: (subst0 (clen c0) t x0
-t2)).(let H8 \def (eq_ind K (Flat f) (\lambda (ee: K).(match ee in K return
-(\lambda (_: K).Prop) with [(Bind _) \Rightarrow False | (Flat _) \Rightarrow
-True])) I (Bind Abbr) H5) in (False_ind (eq T t1 t2) H8)))))) H4)) H3)))))))
-k)) (\lambda (H1: (ex2 T (\lambda (t2: T).((eq T t1 t2) \to (\forall (P:
-Prop).P))) (\lambda (t2: T).(pr2 c0 t1 t2)))).(ex2_ind T (\lambda (t2:
-T).((eq T t1 t2) \to (\forall (P: Prop).P))) (\lambda (t2: T).(pr2 c0 t1 t2))
-(or (\forall (t2: T).((pr2 (CTail k t c0) t1 t2) \to (eq T t1 t2))) (ex2 T
-(\lambda (t2: T).((eq T t1 t2) \to (\forall (P: Prop).P))) (\lambda (t2:
-T).(pr2 (CTail k t c0) t1 t2)))) (\lambda (x: T).(\lambda (H2: (((eq T t1 x)
-\to (\forall (P: Prop).P)))).(\lambda (H3: (pr2 c0 t1 x)).(or_intror (\forall
+T).(subst0 (clen c0) t t0 t2)) (eq T t1 t2) (\lambda (x0: T).(\lambda (H5:
+(eq K (Flat f) (Bind Abbr))).(\lambda (_: (pr0 t1 x0)).(\lambda (_: (subst0
+(clen c0) t x0 t2)).(let H8 \def (eq_ind K (Flat f) (\lambda (ee: K).(match
+ee with [(Bind _) \Rightarrow False | (Flat _) \Rightarrow True])) I (Bind
+Abbr) H5) in (False_ind (eq T t1 t2) H8)))))) H4)) H3))))))) k)) (\lambda
+(H1: (ex2 T (\lambda (t2: T).((eq T t1 t2) \to (\forall (P: Prop).P)))
+(\lambda (t2: T).(pr2 c0 t1 t2)))).(ex2_ind T (\lambda (t2: T).((eq T t1 t2)
+\to (\forall (P: Prop).P))) (\lambda (t2: T).(pr2 c0 t1 t2)) (or (\forall
(t2: T).((pr2 (CTail k t c0) t1 t2) \to (eq T t1 t2))) (ex2 T (\lambda (t2:
T).((eq T t1 t2) \to (\forall (P: Prop).P))) (\lambda (t2: T).(pr2 (CTail k t
-c0) t1 t2))) (ex_intro2 T (\lambda (t2: T).((eq T t1 t2) \to (\forall (P:
-Prop).P))) (\lambda (t2: T).(pr2 (CTail k t c0) t1 t2)) x H2 (pr2_ctail c0 t1
-x H3 k t)))))) H1)) H0)))))))) c).
-(* COMMENTS
-Initial nodes: 3653
-END *)
+c0) t1 t2)))) (\lambda (x: T).(\lambda (H2: (((eq T t1 x) \to (\forall (P:
+Prop).P)))).(\lambda (H3: (pr2 c0 t1 x)).(or_intror (\forall (t2: T).((pr2
+(CTail k t c0) t1 t2) \to (eq T t1 t2))) (ex2 T (\lambda (t2: T).((eq T t1
+t2) \to (\forall (P: Prop).P))) (\lambda (t2: T).(pr2 (CTail k t c0) t1 t2)))
+(ex_intro2 T (\lambda (t2: T).((eq T t1 t2) \to (\forall (P: Prop).P)))
+(\lambda (t2: T).(pr2 (CTail k t c0) t1 t2)) x H2 (pr2_ctail c0 t1 x H3 k
+t)))))) H1)) H0)))))))) c).