(* This file was automatically generated: do not edit *********************)
-include "LambdaDelta-1/T/defs.ma".
+include "Basic-1/T/defs.ma".
theorem terms_props__bind_dec:
\forall (b1: B).(\forall (b2: B).(or (eq B b1 b2) ((eq B b1 b2) \to (\forall
Abst \Rightarrow False | Void \Rightarrow True])) I Abst H) in (False_ind P
H0))))) (or_introl (eq B Void Void) ((eq B Void Void) \to (\forall (P:
Prop).P)) (refl_equal B Void)) b2)) b1).
+(* COMMENTS
+Initial nodes: 559
+END *)
theorem bind_dec_not:
\forall (b1: B).(\forall (b2: B).(or (eq B b1 b2) (not (eq B b1 b2))))
b2)).(or_introl (eq B b1 b2) ((eq B b1 b2) \to False) H0)) (\lambda (H0:
(((eq B b1 b2) \to (\forall (P: Prop).P)))).(or_intror (eq B b1 b2) ((eq B b1
b2) \to False) (\lambda (H1: (eq B b1 b2)).(H0 H1 False)))) H)))).
+(* COMMENTS
+Initial nodes: 131
+END *)
theorem terms_props__flat_dec:
\forall (f1: F).(\forall (f2: F).(or (eq F f1 f2) ((eq F f1 f2) \to (\forall
\Rightarrow True])) I Appl H) in (False_ind P H0))))) (or_introl (eq F Cast
Cast) ((eq F Cast Cast) \to (\forall (P: Prop).P)) (refl_equal F Cast)) f2))
f1).
+(* COMMENTS
+Initial nodes: 263
+END *)
theorem terms_props__kind_dec:
\forall (k1: K).(\forall (k2: K).(or (eq K k1 k2) ((eq K k1 k2) \to (\forall
[(Bind _) \Rightarrow f | (Flat f1) \Rightarrow f1])) (Flat f) (Flat f0) H1)
in (let H3 \def (eq_ind_r F f0 (\lambda (f1: F).((eq F f f1) \to (\forall
(P0: Prop).P0))) H0 f H2) in (H3 (refl_equal F f) P))))))) H)))) k2))) k1).
+(* COMMENTS
+Initial nodes: 799
+END *)
theorem term_dec:
\forall (t1: T).(\forall (t2: T).(or (eq T t1 t2) ((eq T t1 t2) \to (\forall
(let H13 \def (eq_ind_r T t3 (\lambda (t5: T).(or (eq T (THead k t t0) t5)
((eq T (THead k t t0) t5) \to (\forall (P0: Prop).P0)))) H1 t H9) in (H12
(refl_equal T t) P))))))) H7)) H6)))))) H3)))))))) t2))))))) t1).
+(* COMMENTS
+Initial nodes: 2821
+END *)
theorem binder_dec:
\forall (t: T).(or (ex_3 B T T (\lambda (b: B).(\lambda (w: T).(\lambda (u:
\Rightarrow (match k0 in K return (\lambda (_: K).Prop) with [(Bind _)
\Rightarrow False | (Flat _) \Rightarrow True])])) I (THead (Bind b) w u) H1)
in (False_ind P H2))))))))))))) k)) t).
+(* COMMENTS
+Initial nodes: 1063
+END *)
theorem abst_dec:
\forall (u: T).(\forall (v: T).(or (ex T (\lambda (t: T).(eq T u (THead
\Rightarrow t2])) (THead k t t0) (THead (Bind Abst) v t1) H3) in (\lambda (_:
(eq T t v)).(\lambda (H8: (eq K k (Bind Abst))).(H2 H8 P)))) H5)) H4)))))))
H1))))))))) u).
+(* COMMENTS
+Initial nodes: 1305
+END *)