(* This file was automatically generated: do not edit *********************)
-include "LambdaDelta-1/T/defs.ma".
+include "Basic-1/T/defs.ma".
theorem not_abbr_abst:
not (eq B Abbr Abst)
B).(match ee in B return (\lambda (_: B).Prop) with [Abbr \Rightarrow True |
Abst \Rightarrow False | Void \Rightarrow False])) I Abst H) in (False_ind
False H0)).
+(* COMMENTS
+Initial nodes: 34
+END *)
theorem not_void_abst:
not (eq B Void Abst)
B).(match ee in B return (\lambda (_: B).Prop) with [Abbr \Rightarrow False |
Abst \Rightarrow False | Void \Rightarrow True])) I Abst H) in (False_ind
False H0)).
+(* COMMENTS
+Initial nodes: 34
+END *)
theorem not_abbr_void:
not (eq B Abbr Void)
B).(match ee in B return (\lambda (_: B).Prop) with [Abbr \Rightarrow True |
Abst \Rightarrow False | Void \Rightarrow False])) I Void H) in (False_ind
False H0)).
+(* COMMENTS
+Initial nodes: 34
+END *)
theorem not_abst_void:
not (eq B Abst Void)
B).(match ee in B return (\lambda (_: B).Prop) with [Abbr \Rightarrow False |
Abst \Rightarrow True | Void \Rightarrow False])) I Void H) in (False_ind
False H0)).
+(* COMMENTS
+Initial nodes: 34
+END *)
theorem thead_x_y_y:
\forall (k: K).(\forall (v: T).(\forall (t: T).((eq T (THead k v t) t) \to
H0 t0 H5) in (let H8 \def (eq_ind K k (\lambda (k1: K).((eq T (THead k1 t0
t1) t1) \to (\forall (P0: Prop).P0))) H7 k0 H6) in (H8 H4 P)))))) H3))
H2))))))))) t))).
+(* COMMENTS
+Initial nodes: 461
+END *)
theorem tweight_lt:
\forall (t: T).(lt O (tweight t))
(t0: T).(\lambda (H: (lt O (tweight t0))).(\lambda (t1: T).(\lambda (_: (lt O
(tweight t1))).(le_S (S O) (plus (tweight t0) (tweight t1)) (le_plus_trans (S
O) (tweight t0) (tweight t1) H))))))) t).
+(* COMMENTS
+Initial nodes: 85
+END *)