Base.ma now ok!!

diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/Base.ma b/matita/contribs/LAMBDA-TYPES/Level-1/Base.ma
index 4e8b785f6abd60f3a362416d7fb191b86ed12175..7380acd2886a934f582aadb0f3302158333dd875 100644 (file)
--- a/matita/contribs/LAMBDA-TYPES/Level-1/Base.ma
+++ b/matita/contribs/LAMBDA-TYPES/Level-1/Base.ma
@@ -61,7 +61,7 @@ theorem plus_permute_2_in_3_assoc:
 theorem plus_O:
  \forall (x: nat).(\forall (y: nat).((eq nat (plus x y) O) \to (land (eq nat x O) (eq nat y O))))
 \def
- \lambda (x: nat).(nat_ind (\lambda (n: nat).(\forall (y: nat).((eq nat (plus n y) O) \to (land (eq nat n O) (eq nat y O))))) (\lambda (y: nat).(\lambda (H: (eq nat (plus O y) O)).(conj (eq nat O O) (eq nat y O) (refl_equal nat O) H))) (\lambda (n: nat).(\lambda (_: ((\forall (y: nat).((eq nat (plus n y) O) \to (land (eq nat n O) (eq nat y O)))))).(\lambda (y: nat).(\lambda (H0: (eq nat (plus (S n) y) O)).(let H1 \def (match H0 return (\lambda (_: ?).(\lambda (n0: nat).((eq nat n0 O) \to (land (eq nat (S n) O) (eq nat y O))))) with [refl_equal \Rightarrow (\lambda (H1: (eq nat (plus (S n) y) O)).(let H2 \def (eq_ind nat (plus (S n) y) (\lambda (e: nat).(match e return (\lambda (_: ?).Prop) with [O \Rightarrow False | (S _) \Rightarrow True])) I O H1) in (False_ind (land (eq nat (S n) O) (eq nat y O)) H2)))]) in (H1 (refl_equal nat O))))))) x).
+ \lambda (x: nat).(nat_ind (\lambda (n: nat).(\forall (y: nat).((eq nat (plus n y) O) \to (land (eq nat n O) (eq nat y O))))) (\lambda (y: nat).(\lambda (H: (eq nat (plus O y) O)).(conj (eq nat O O) (eq nat y O) (refl_equal nat O) H))) (\lambda (n: nat).(\lambda (_: ((\forall (y: nat).((eq nat (plus n y) O) \to (land (eq nat n O) (eq nat y O)))))).(\lambda (y: nat).(\lambda (H0: (eq nat (plus (S n) y) O)).(let H1 \def (match H0 return (\lambda (n0: nat).(\lambda (_: (eq ? ? n0)).((eq nat n0 O) \to (land (eq nat (S n) O) (eq nat y O))))) with [refl_equal \Rightarrow (\lambda (H1: (eq nat (plus (S n) y) O)).(let H2 \def (eq_ind nat (plus (S n) y) (\lambda (e: nat).(match e return (\lambda (_: ?).Prop) with [O \Rightarrow False | (S _) \Rightarrow True])) I O H1) in (False_ind (land (eq nat (S n) O) (eq nat y O)) H2)))]) in (H1 (refl_equal nat O))))))) x).
 
 theorem minus_Sx_SO:
  \forall (x: nat).(eq nat (minus (S x) (S O)) x)
@@ -81,7 +81,7 @@ theorem neq_eq_e:
 theorem le_false:
  \forall (m: nat).(\forall (n: nat).(\forall (P: Prop).((le m n) \to ((le (S n) m) \to P))))
 \def
- \lambda (m: nat).(nat_ind (\lambda (n: nat).(\forall (n0: nat).(\forall (P: Prop).((le n n0) \to ((le (S n0) n) \to P))))) (\lambda (n: nat).(\lambda (P: Prop).(\lambda (_: (le O n)).(\lambda (H0: (le (S n) O)).(let H1 \def (match H0 return (\lambda (_: ?).(\lambda (n: nat).((eq nat n O) \to P))) with [le_n \Rightarrow (\lambda (H1: (eq nat (S n) O)).(let H2 \def (eq_ind nat (S n) (\lambda (e: nat).(match e return (\lambda (_: ?).Prop) with [O \Rightarrow False | (S _) \Rightarrow True])) I O H1) in (False_ind P H2))) | (le_S m H1) \Rightarrow (\lambda (H2: (eq nat (S m) O)).((let H3 \def (eq_ind nat (S m) (\lambda (e: nat).(match e return (\lambda (_: ?).Prop) with [O \Rightarrow False | (S _) \Rightarrow True])) I O H2) in (False_ind ((le (S n) m) \to P) H3)) H1))]) in (H1 (refl_equal nat O))))))) (\lambda (n: nat).(\lambda (H: ((\forall (n0: nat).(\forall (P: Prop).((le n n0) \to ((le (S n0) n) \to P)))))).(\lambda (n0: nat).(nat_ind (\lambda (n1: nat).(\forall (P: Prop).((le (S n) n1) \to ((le (S n1) (S n)) \to P)))) (\lambda (P: Prop).(\lambda (H0: (le (S n) O)).(\lambda (_: (le (S O) (S n))).(let H2 \def (match H0 return (\lambda (_: ?).(\lambda (n: nat).((eq nat n O) \to P))) with [le_n \Rightarrow (\lambda (H2: (eq nat (S n) O)).(let H3 \def (eq_ind nat (S n) (\lambda (e: nat).(match e return (\lambda (_: ?).Prop) with [O \Rightarrow False | (S _) \Rightarrow True])) I O H2) in (False_ind P H3))) | (le_S m H2) \Rightarrow (\lambda (H3: (eq nat (S m) O)).((let H4 \def (eq_ind nat (S m) (\lambda (e: nat).(match e return (\lambda (_: ?).Prop) with [O \Rightarrow False | (S _) \Rightarrow True])) I O H3) in (False_ind ((le (S n) m) \to P) H4)) H2))]) in (H2 (refl_equal nat O)))))) (\lambda (n1: nat).(\lambda (_: ((\forall (P: Prop).((le (S n) n1) \to ((le (S n1) (S n)) \to P))))).(\lambda (P: Prop).(\lambda (H1: (le (S n) (S n1))).(\lambda (H2: (le (S (S n1)) (S n))).(H n1 P (le_S_n n n1 H1) (le_S_n (S n1) n H2))))))) n0)))) m).
+ \lambda (m: nat).(nat_ind (\lambda (n: nat).(\forall (n0: nat).(\forall (P: Prop).((le n n0) \to ((le (S n0) n) \to P))))) (\lambda (n: nat).(\lambda (P: Prop).(\lambda (_: (le O n)).(\lambda (H0: (le (S n) O)).(let H1 \def (match H0 return (\lambda (n: nat).(\lambda (_: (le ? n)).((eq nat n O) \to P))) with [le_n \Rightarrow (\lambda (H1: (eq nat (S n) O)).(let H2 \def (eq_ind nat (S n) (\lambda (e: nat).(match e return (\lambda (_: ?).Prop) with [O \Rightarrow False | (S _) \Rightarrow True])) I O H1) in (False_ind P H2))) | (le_S m H1) \Rightarrow (\lambda (H2: (eq nat (S m) O)).((let H3 \def (eq_ind nat (S m) (\lambda (e: nat).(match e return (\lambda (_: ?).Prop) with [O \Rightarrow False | (S _) \Rightarrow True])) I O H2) in (False_ind ((le (S n) m) \to P) H3)) H1))]) in (H1 (refl_equal nat O))))))) (\lambda (n: nat).(\lambda (H: ((\forall (n0: nat).(\forall (P: Prop).((le n n0) \to ((le (S n0) n) \to P)))))).(\lambda (n0: nat).(nat_ind (\lambda (n1: nat).(\forall (P: Prop).((le (S n) n1) \to ((le (S n1) (S n)) \to P)))) (\lambda (P: Prop).(\lambda (H0: (le (S n) O)).(\lambda (_: (le (S O) (S n))).(let H2 \def (match H0 return (\lambda (n: nat).(\lambda (_: (le ? n)).((eq nat n O) \to P))) with [le_n \Rightarrow (\lambda (H2: (eq nat (S n) O)).(let H3 \def (eq_ind nat (S n) (\lambda (e: nat).(match e return (\lambda (_: ?).Prop) with [O \Rightarrow False | (S _) \Rightarrow True])) I O H2) in (False_ind P H3))) | (le_S m H2) \Rightarrow (\lambda (H3: (eq nat (S m) O)).((let H4 \def (eq_ind nat (S m) (\lambda (e: nat).(match e return (\lambda (_: ?).Prop) with [O \Rightarrow False | (S _) \Rightarrow True])) I O H3) in (False_ind ((le (S n) m) \to P) H4)) H2))]) in (H2 (refl_equal nat O)))))) (\lambda (n1: nat).(\lambda (_: ((\forall (P: Prop).((le (S n) n1) \to ((le (S n1) (S n)) \to P))))).(\lambda (P: Prop).(\lambda (H1: (le (S n) (S n1))).(\lambda (H2: (le (S (S n1)) (S n))).(H n1 P (le_S_n n n1 H1) (le_S_n (S n1) n H2))))))) n0)))) m).
 
 theorem le_Sx_x:
  \forall (x: nat).((le (S x) x) \to (\forall (P: Prop).P))
@@ -91,7 +91,7 @@ theorem le_Sx_x:
 theorem minus_le:
  \forall (x: nat).(\forall (y: nat).(le (minus x y) x))
 \def
- \lambda (x: nat).(nat_ind (\lambda (n: nat).(\forall (y: nat).(le (minus n y) n))) (\lambda (_: nat).(le_n O)) (\lambda (n: nat).(\lambda (H: ((\forall (y: nat).(le (minus n y) n)))).(\lambda (y: nat).(match y return (\lambda (_: ?).(\lambda (n0: nat).(le (minus (S n) n0) (S n)))) with [O \Rightarrow (le_n (S n)) | (S n0) \Rightarrow (le_S (minus n n0) n (H n0))])))) x).
+ \lambda (x: nat).(nat_ind (\lambda (n: nat).(\forall (y: nat).(le (minus n y) n))) (\lambda (_: nat).(le_n O)) (\lambda (n: nat).(\lambda (H: ((\forall (y: nat).(le (minus n y) n)))).(\lambda (y: nat).(match y return (\lambda (n0: nat).(le (minus (S n) n0) (S n))) with [O \Rightarrow (le_n (S n)) | (S n0) \Rightarrow (le_S (minus n n0) n (H n0))])))) x).
 
 theorem le_plus_minus_sym:
  \forall (n: nat).(\forall (m: nat).((le n m) \to (eq nat m (plus (minus m n) n))))
@@ -106,7 +106,7 @@ theorem le_minus_minus:
 theorem le_minus_plus:
  \forall (z: nat).(\forall (x: nat).((le z x) \to (\forall (y: nat).(eq nat (minus (plus x y) z) (plus (minus x z) y)))))
 \def
- \lambda (z: nat).(nat_ind (\lambda (n: nat).(\forall (x: nat).((le n x) \to (\forall (y: nat).(eq nat (minus (plus x y) n) (plus (minus x n) y)))))) (\lambda (x: nat).(\lambda (H: (le O x)).(let H0 \def (match H return (\lambda (_: ?).(\lambda (n: nat).((eq nat n x) \to (\forall (y: nat).(eq nat (minus (plus x y) O) (plus (minus x O) y)))))) with [le_n \Rightarrow (\lambda (H0: (eq nat O x)).(eq_ind nat O (\lambda (n: nat).(\forall (y: nat).(eq nat (minus (plus n y) O) (plus (minus n O) y)))) (\lambda (y: nat).(sym_eq nat (plus (minus O O) y) (minus (plus O y) O) (minus_n_O (plus O y)))) x H0)) | (le_S m H0) \Rightarrow (\lambda (H1: (eq nat (S m) x)).(eq_ind nat (S m) (\lambda (n: nat).((le O m) \to (\forall (y: nat).(eq nat (minus (plus n y) O) (plus (minus n O) y))))) (\lambda (_: (le O m)).(\lambda (y: nat).(refl_equal nat (plus (minus (S m) O) y)))) x H1 H0))]) in (H0 (refl_equal nat x))))) (\lambda (z0: nat).(\lambda (H: ((\forall (x: nat).((le z0 x) \to (\forall (y: nat).(eq nat (minus (plus x y) z0) (plus (minus x z0) y))))))).(\lambda (x: nat).(nat_ind (\lambda (n: nat).((le (S z0) n) \to (\forall (y: nat).(eq nat (minus (plus n y) (S z0)) (plus (minus n (S z0)) y))))) (\lambda (H0: (le (S z0) O)).(\lambda (y: nat).(let H1 \def (match H0 return (\lambda (_: ?).(\lambda (n: nat).((eq nat n O) \to (eq nat (minus (plus O y) (S z0)) (plus (minus O (S z0)) y))))) with [le_n \Rightarrow (\lambda (H1: (eq nat (S z0) O)).(let H2 \def (eq_ind nat (S z0) (\lambda (e: nat).(match e return (\lambda (_: ?).Prop) with [O \Rightarrow False | (S _) \Rightarrow True])) I O H1) in (False_ind (eq nat (minus (plus O y) (S z0)) (plus (minus O (S z0)) y)) H2))) | (le_S m H1) \Rightarrow (\lambda (H2: (eq nat (S m) O)).((let H3 \def (eq_ind nat (S m) (\lambda (e: nat).(match e return (\lambda (_: ?).Prop) with [O \Rightarrow False | (S _) \Rightarrow True])) I O H2) in (False_ind ((le (S z0) m) \to (eq nat (minus (plus O y) (S z0)) (plus (minus O (S z0)) y))) H3)) H1))]) in (H1 (refl_equal nat O))))) (\lambda (n: nat).(\lambda (_: (((le (S z0) n) \to (\forall (y: nat).(eq nat (minus (plus n y) (S z0)) (plus (minus n (S z0)) y)))))).(\lambda (H1: (le (S z0) (S n))).(\lambda (y: nat).(H n (le_S_n z0 n H1) y))))) x)))) z).
+ \lambda (z: nat).(nat_ind (\lambda (n: nat).(\forall (x: nat).((le n x) \to (\forall (y: nat).(eq nat (minus (plus x y) n) (plus (minus x n) y)))))) (\lambda (x: nat).(\lambda (H: (le O x)).(let H0 \def (match H return (\lambda (n: nat).(\lambda (_: (le ? n)).((eq nat n x) \to (\forall (y: nat).(eq nat (minus (plus x y) O) (plus (minus x O) y)))))) with [le_n \Rightarrow (\lambda (H0: (eq nat O x)).(eq_ind nat O (\lambda (n: nat).(\forall (y: nat).(eq nat (minus (plus n y) O) (plus (minus n O) y)))) (\lambda (y: nat).(sym_eq nat (plus (minus O O) y) (minus (plus O y) O) (minus_n_O (plus O y)))) x H0)) | (le_S m H0) \Rightarrow (\lambda (H1: (eq nat (S m) x)).(eq_ind nat (S m) (\lambda (n: nat).((le O m) \to (\forall (y: nat).(eq nat (minus (plus n y) O) (plus (minus n O) y))))) (\lambda (_: (le O m)).(\lambda (y: nat).(refl_equal nat (plus (minus (S m) O) y)))) x H1 H0))]) in (H0 (refl_equal nat x))))) (\lambda (z0: nat).(\lambda (H: ((\forall (x: nat).((le z0 x) \to (\forall (y: nat).(eq nat (minus (plus x y) z0) (plus (minus x z0) y))))))).(\lambda (x: nat).(nat_ind (\lambda (n: nat).((le (S z0) n) \to (\forall (y: nat).(eq nat (minus (plus n y) (S z0)) (plus (minus n (S z0)) y))))) (\lambda (H0: (le (S z0) O)).(\lambda (y: nat).(let H1 \def (match H0 return (\lambda (n: nat).(\lambda (_: (le ? n)).((eq nat n O) \to (eq nat (minus (plus O y) (S z0)) (plus (minus O (S z0)) y))))) with [le_n \Rightarrow (\lambda (H1: (eq nat (S z0) O)).(let H2 \def (eq_ind nat (S z0) (\lambda (e: nat).(match e return (\lambda (_: ?).Prop) with [O \Rightarrow False | (S _) \Rightarrow True])) I O H1) in (False_ind (eq nat (minus (plus O y) (S z0)) (plus (minus O (S z0)) y)) H2))) | (le_S m H1) \Rightarrow (\lambda (H2: (eq nat (S m) O)).((let H3 \def (eq_ind nat (S m) (\lambda (e: nat).(match e return (\lambda (_: ?).Prop) with [O \Rightarrow False | (S _) \Rightarrow True])) I O H2) in (False_ind ((le (S z0) m) \to (eq nat (minus (plus O y) (S z0)) (plus (minus O (S z0)) y))) H3)) H1))]) in (H1 (refl_equal nat O))))) (\lambda (n: nat).(\lambda (_: (((le (S z0) n) \to (\forall (y: nat).(eq nat (minus (plus n y) (S z0)) (plus (minus n (S z0)) y)))))).(\lambda (H1: (le (S z0) (S n))).(\lambda (y: nat).(H n (le_S_n z0 n H1) y))))) x)))) z).
 
 theorem le_minus:
  \forall (x: nat).(\forall (z: nat).(\forall (y: nat).((le (plus x y) z) \to (le x (minus z y)))))
@@ -121,7 +121,7 @@ theorem le_trans_plus_r:
 theorem le_gen_S:
  \forall (m: nat).(\forall (x: nat).((le (S m) x) \to (ex2 nat (\lambda (n: nat).(eq nat x (S n))) (\lambda (n: nat).(le m n)))))
 \def
- \lambda (m: nat).(\lambda (x: nat).(\lambda (H: (le (S m) x)).(let H0 \def (match H return (\lambda (_: ?).(\lambda (n: nat).((eq nat n x) \to (ex2 nat (\lambda (n0: nat).(eq nat x (S n0))) (\lambda (n0: nat).(le m n0)))))) with [le_n \Rightarrow (\lambda (H0: (eq nat (S m) x)).(eq_ind nat (S m) (\lambda (n: nat).(ex2 nat (\lambda (n0: nat).(eq nat n (S n0))) (\lambda (n0: nat).(le m n0)))) (ex_intro2 nat (\lambda (n: nat).(eq nat (S m) (S n))) (\lambda (n: nat).(le m n)) m (refl_equal nat (S m)) (le_n m)) x H0)) | (le_S m0 H0) \Rightarrow (\lambda (H1: (eq nat (S m0) x)).(eq_ind nat (S m0) (\lambda (n: nat).((le (S m) m0) \to (ex2 nat (\lambda (n0: nat).(eq nat n (S n0))) (\lambda (n0: nat).(le m n0))))) (\lambda (H2: (le (S m) m0)).(ex_intro2 nat (\lambda (n: nat).(eq nat (S m0) (S n))) (\lambda (n: nat).(le m n)) m0 (refl_equal nat (S m0)) (le_S_n m m0 (le_S (S m) m0 H2)))) x H1 H0))]) in (H0 (refl_equal nat x))))).
+ \lambda (m: nat).(\lambda (x: nat).(\lambda (H: (le (S m) x)).(let H0 \def (match H return (\lambda (n: nat).(\lambda (_: (le ? n)).((eq nat n x) \to (ex2 nat (\lambda (n0: nat).(eq nat x (S n0))) (\lambda (n0: nat).(le m n0)))))) with [le_n \Rightarrow (\lambda (H0: (eq nat (S m) x)).(eq_ind nat (S m) (\lambda (n: nat).(ex2 nat (\lambda (n0: nat).(eq nat n (S n0))) (\lambda (n0: nat).(le m n0)))) (ex_intro2 nat (\lambda (n: nat).(eq nat (S m) (S n))) (\lambda (n: nat).(le m n)) m (refl_equal nat (S m)) (le_n m)) x H0)) | (le_S m0 H0) \Rightarrow (\lambda (H1: (eq nat (S m0) x)).(eq_ind nat (S m0) (\lambda (n: nat).((le (S m) m0) \to (ex2 nat (\lambda (n0: nat).(eq nat n (S n0))) (\lambda (n0: nat).(le m n0))))) (\lambda (H2: (le (S m) m0)).(ex_intro2 nat (\lambda (n: nat).(eq nat (S m0) (S n))) (\lambda (n: nat).(le m n)) m0 (refl_equal nat (S m0)) (le_S_n m m0 (le_S (S m) m0 H2)))) x H1 H0))]) in (H0 (refl_equal nat x))))).
 
 theorem lt_x_plus_x_Sy:
  \forall (x: nat).(\forall (y: nat).(lt x (plus x (S y))))
@@ -136,7 +136,7 @@ theorem simpl_lt_plus_r:
 theorem minus_x_Sy:
  \forall (x: nat).(\forall (y: nat).((lt y x) \to (eq nat (minus x y) (S (minus x (S y))))))
 \def
- \lambda (x: nat).(nat_ind (\lambda (n: nat).(\forall (y: nat).((lt y n) \to (eq nat (minus n y) (S (minus n (S y))))))) (\lambda (y: nat).(\lambda (H: (lt y O)).(let H0 \def (match H return (\lambda (_: ?).(\lambda (n: nat).((eq nat n O) \to (eq nat (minus O y) (S (minus O (S y))))))) with [le_n \Rightarrow (\lambda (H0: (eq nat (S y) O)).(let H1 \def (eq_ind nat (S y) (\lambda (e: nat).(match e return (\lambda (_: ?).Prop) with [O \Rightarrow False | (S _) \Rightarrow True])) I O H0) in (False_ind (eq nat (minus O y) (S (minus O (S y)))) H1))) | (le_S m H0) \Rightarrow (\lambda (H1: (eq nat (S m) O)).((let H2 \def (eq_ind nat (S m) (\lambda (e: nat).(match e return (\lambda (_: ?).Prop) with [O \Rightarrow False | (S _) \Rightarrow True])) I O H1) in (False_ind ((le (S y) m) \to (eq nat (minus O y) (S (minus O (S y))))) H2)) H0))]) in (H0 (refl_equal nat O))))) (\lambda (n: nat).(\lambda (H: ((\forall (y: nat).((lt y n) \to (eq nat (minus n y) (S (minus n (S y)))))))).(\lambda (y: nat).(nat_ind (\lambda (n0: nat).((lt n0 (S n)) \to (eq nat (minus (S n) n0) (S (minus (S n) (S n0)))))) (\lambda (_: (lt O (S n))).(eq_ind nat n (\lambda (n0: nat).(eq nat (S n) (S n0))) (refl_equal nat (S n)) (minus n O) (minus_n_O n))) (\lambda (n0: nat).(\lambda (_: (((lt n0 (S n)) \to (eq nat (minus (S n) n0) (S (minus (S n) (S n0))))))).(\lambda (H1: (lt (S n0) (S n))).(let H2 \def (le_S_n (S n0) n H1) in (H n0 H2))))) y)))) x).
+ \lambda (x: nat).(nat_ind (\lambda (n: nat).(\forall (y: nat).((lt y n) \to (eq nat (minus n y) (S (minus n (S y))))))) (\lambda (y: nat).(\lambda (H: (lt y O)).(let H0 \def (match H return (\lambda (n: nat).(\lambda (_: (lt ? n)).((eq nat n O) \to (eq nat (minus O y) (S (minus O (S y))))))) with [le_n \Rightarrow (\lambda (H0: (eq nat (S y) O)).(let H1 \def (eq_ind nat (S y) (\lambda (e: nat).(match e return (\lambda (_: ?).Prop) with [O \Rightarrow False | (S _) \Rightarrow True])) I O H0) in (False_ind (eq nat (minus O y) (S (minus O (S y)))) H1))) | (le_S m H0) \Rightarrow (\lambda (H1: (eq nat (S m) O)).((let H2 \def (eq_ind nat (S m) (\lambda (e: nat).(match e return (\lambda (_: ?).Prop) with [O \Rightarrow False | (S _) \Rightarrow True])) I O H1) in (False_ind ((le (S y) m) \to (eq nat (minus O y) (S (minus O (S y))))) H2)) H0))]) in (H0 (refl_equal nat O))))) (\lambda (n: nat).(\lambda (H: ((\forall (y: nat).((lt y n) \to (eq nat (minus n y) (S (minus n (S y)))))))).(\lambda (y: nat).(nat_ind (\lambda (n0: nat).((lt n0 (S n)) \to (eq nat (minus (S n) n0) (S (minus (S n) (S n0)))))) (\lambda (_: (lt O (S n))).(eq_ind nat n (\lambda (n0: nat).(eq nat (S n) (S n0))) (refl_equal nat (S n)) (minus n O) (minus_n_O n))) (\lambda (n0: nat).(\lambda (_: (((lt n0 (S n)) \to (eq nat (minus (S n) n0) (S (minus (S n) (S n0))))))).(\lambda (H1: (lt (S n0) (S n))).(let H2 \def (le_S_n (S n0) n H1) in (H n0 H2))))) y)))) x).
 
 theorem lt_plus_minus:
  \forall (x: nat).(\forall (y: nat).((lt x y) \to (eq nat y (S (plus x (minus y (S x)))))))
@@ -156,7 +156,7 @@ theorem minus_x_SO:
 theorem le_x_pred_y:
  \forall (y: nat).(\forall (x: nat).((lt x y) \to (le x (pred y))))
 \def
- \lambda (y: nat).(nat_ind (\lambda (n: nat).(\forall (x: nat).((lt x n) \to (le x (pred n))))) (\lambda (x: nat).(\lambda (H: (lt x O)).(let H0 \def (match H return (\lambda (_: ?).(\lambda (n: nat).((eq nat n O) \to (le x O)))) with [le_n \Rightarrow (\lambda (H0: (eq nat (S x) O)).(let H1 \def (eq_ind nat (S x) (\lambda (e: nat).(match e return (\lambda (_: ?).Prop) with [O \Rightarrow False | (S _) \Rightarrow True])) I O H0) in (False_ind (le x O) H1))) | (le_S m H0) \Rightarrow (\lambda (H1: (eq nat (S m) O)).((let H2 \def (eq_ind nat (S m) (\lambda (e: nat).(match e return (\lambda (_: ?).Prop) with [O \Rightarrow False | (S _) \Rightarrow True])) I O H1) in (False_ind ((le (S x) m) \to (le x O)) H2)) H0))]) in (H0 (refl_equal nat O))))) (\lambda (n: nat).(\lambda (_: ((\forall (x: nat).((lt x n) \to (le x (pred n)))))).(\lambda (x: nat).(\lambda (H0: (lt x (S n))).(le_S_n x n H0))))) y).
+ \lambda (y: nat).(nat_ind (\lambda (n: nat).(\forall (x: nat).((lt x n) \to (le x (pred n))))) (\lambda (x: nat).(\lambda (H: (lt x O)).(let H0 \def (match H return (\lambda (n: nat).(\lambda (_: (lt ? n)).((eq nat n O) \to (le x O)))) with [le_n \Rightarrow (\lambda (H0: (eq nat (S x) O)).(let H1 \def (eq_ind nat (S x) (\lambda (e: nat).(match e return (\lambda (_: ?).Prop) with [O \Rightarrow False | (S _) \Rightarrow True])) I O H0) in (False_ind (le x O) H1))) | (le_S m H0) \Rightarrow (\lambda (H1: (eq nat (S m) O)).((let H2 \def (eq_ind nat (S m) (\lambda (e: nat).(match e return (\lambda (_: ?).Prop) with [O \Rightarrow False | (S _) \Rightarrow True])) I O H1) in (False_ind ((le (S x) m) \to (le x O)) H2)) H0))]) in (H0 (refl_equal nat O))))) (\lambda (n: nat).(\lambda (_: ((\forall (x: nat).((lt x n) \to (le x (pred n)))))).(\lambda (x: nat).(\lambda (H0: (lt x (S n))).(le_S_n x n H0))))) y).
 
 theorem lt_le_minus:
  \forall (x: nat).(\forall (y: nat).((lt x y) \to (le x (minus y (S O)))))
@@ -288,20 +288,20 @@ definition blt:
 theorem lt_blt:
  \forall (x: nat).(\forall (y: nat).((lt y x) \to (eq bool (blt y x) true)))
 \def
- \lambda (x: nat).(nat_ind (\lambda (n: nat).(\forall (y: nat).((lt y n) \to (eq bool (blt y n) true)))) (\lambda (y: nat).(\lambda (H: (lt y O)).(let H0 \def (match H return (\lambda (_: ?).(\lambda (n: nat).((eq nat n O) \to (eq bool (blt y O) true)))) with [le_n \Rightarrow (\lambda (H0: (eq nat (S y) O)).(let H1 \def (eq_ind nat (S y) (\lambda (e: nat).(match e return (\lambda (_: ?).Prop) with [O \Rightarrow False | (S _) \Rightarrow True])) I O H0) in (False_ind (eq bool (blt y O) true) H1))) | (le_S m H0) \Rightarrow (\lambda (H1: (eq nat (S m) O)).((let H2 \def (eq_ind nat (S m) (\lambda (e: nat).(match e return (\lambda (_: ?).Prop) with [O \Rightarrow False | (S _) \Rightarrow True])) I O H1) in (False_ind ((le (S y) m) \to (eq bool (blt y O) true)) H2)) H0))]) in (H0 (refl_equal nat O))))) (\lambda (n: nat).(\lambda (H: ((\forall (y: nat).((lt y n) \to (eq bool (blt y n) true))))).(\lambda (y: nat).(nat_ind (\lambda (n0: nat).((lt n0 (S n)) \to (eq bool (blt n0 (S n)) true))) (\lambda (_: (lt O (S n))).(refl_equal bool true)) (\lambda (n0: nat).(\lambda (_: (((lt n0 (S n)) \to (eq bool (match n0 with [O \Rightarrow true | (S m) \Rightarrow (blt m n)]) true)))).(\lambda (H1: (lt (S n0) (S n))).(H n0 (le_S_n (S n0) n H1))))) y)))) x).
+ \lambda (x: nat).(nat_ind (\lambda (n: nat).(\forall (y: nat).((lt y n) \to (eq bool (blt y n) true)))) (\lambda (y: nat).(\lambda (H: (lt y O)).(let H0 \def (match H return (\lambda (n: nat).(\lambda (_: (lt ? n)).((eq nat n O) \to (eq bool (blt y O) true)))) with [le_n \Rightarrow (\lambda (H0: (eq nat (S y) O)).(let H1 \def (eq_ind nat (S y) (\lambda (e: nat).(match e return (\lambda (_: ?).Prop) with [O \Rightarrow False | (S _) \Rightarrow True])) I O H0) in (False_ind (eq bool (blt y O) true) H1))) | (le_S m H0) \Rightarrow (\lambda (H1: (eq nat (S m) O)).((let H2 \def (eq_ind nat (S m) (\lambda (e: nat).(match e return (\lambda (_: ?).Prop) with [O \Rightarrow False | (S _) \Rightarrow True])) I O H1) in (False_ind ((le (S y) m) \to (eq bool (blt y O) true)) H2)) H0))]) in (H0 (refl_equal nat O))))) (\lambda (n: nat).(\lambda (H: ((\forall (y: nat).((lt y n) \to (eq bool (blt y n) true))))).(\lambda (y: nat).(nat_ind (\lambda (n0: nat).((lt n0 (S n)) \to (eq bool (blt n0 (S n)) true))) (\lambda (_: (lt O (S n))).(refl_equal bool true)) (\lambda (n0: nat).(\lambda (_: (((lt n0 (S n)) \to (eq bool (match n0 with [O \Rightarrow true | (S m) \Rightarrow (blt m n)]) true)))).(\lambda (H1: (lt (S n0) (S n))).(H n0 (le_S_n (S n0) n H1))))) y)))) x).
 
 theorem le_bge:
  \forall (x: nat).(\forall (y: nat).((le x y) \to (eq bool (blt y x) false)))
 \def
- \lambda (x: nat).(nat_ind (\lambda (n: nat).(\forall (y: nat).((le n y) \to (eq bool (blt y n) false)))) (\lambda (y: nat).(\lambda (_: (le O y)).(refl_equal bool false))) (\lambda (n: nat).(\lambda (H: ((\forall (y: nat).((le n y) \to (eq bool (blt y n) false))))).(\lambda (y: nat).(nat_ind (\lambda (n0: nat).((le (S n) n0) \to (eq bool (blt n0 (S n)) false))) (\lambda (H0: (le (S n) O)).(let H1 \def (match H0 return (\lambda (_: ?).(\lambda (n0: nat).((eq nat n0 O) \to (eq bool (blt O (S n)) false)))) with [le_n \Rightarrow (\lambda (H1: (eq nat (S n) O)).(let H2 \def (eq_ind nat (S n) (\lambda (e: nat).(match e return (\lambda (_: ?).Prop) with [O \Rightarrow False | (S _) \Rightarrow True])) I O H1) in (False_ind (eq bool (blt O (S n)) false) H2))) | (le_S m H1) \Rightarrow (\lambda (H2: (eq nat (S m) O)).((let H3 \def (eq_ind nat (S m) (\lambda (e: nat).(match e return (\lambda (_: ?).Prop) with [O \Rightarrow False | (S _) \Rightarrow True])) I O H2) in (False_ind ((le (S n) m) \to (eq bool (blt O (S n)) false)) H3)) H1))]) in (H1 (refl_equal nat O)))) (\lambda (n0: nat).(\lambda (_: (((le (S n) n0) \to (eq bool (blt n0 (S n)) false)))).(\lambda (H1: (le (S n) (S n0))).(H n0 (le_S_n n n0 H1))))) y)))) x).
+ \lambda (x: nat).(nat_ind (\lambda (n: nat).(\forall (y: nat).((le n y) \to (eq bool (blt y n) false)))) (\lambda (y: nat).(\lambda (_: (le O y)).(refl_equal bool false))) (\lambda (n: nat).(\lambda (H: ((\forall (y: nat).((le n y) \to (eq bool (blt y n) false))))).(\lambda (y: nat).(nat_ind (\lambda (n0: nat).((le (S n) n0) \to (eq bool (blt n0 (S n)) false))) (\lambda (H0: (le (S n) O)).(let H1 \def (match H0 return (\lambda (n0: nat).(\lambda (_: (le ? n0)).((eq nat n0 O) \to (eq bool (blt O (S n)) false)))) with [le_n \Rightarrow (\lambda (H1: (eq nat (S n) O)).(let H2 \def (eq_ind nat (S n) (\lambda (e: nat).(match e return (\lambda (_: ?).Prop) with [O \Rightarrow False | (S _) \Rightarrow True])) I O H1) in (False_ind (eq bool (blt O (S n)) false) H2))) | (le_S m H1) \Rightarrow (\lambda (H2: (eq nat (S m) O)).((let H3 \def (eq_ind nat (S m) (\lambda (e: nat).(match e return (\lambda (_: ?).Prop) with [O \Rightarrow False | (S _) \Rightarrow True])) I O H2) in (False_ind ((le (S n) m) \to (eq bool (blt O (S n)) false)) H3)) H1))]) in (H1 (refl_equal nat O)))) (\lambda (n0: nat).(\lambda (_: (((le (S n) n0) \to (eq bool (blt n0 (S n)) false)))).(\lambda (H1: (le (S n) (S n0))).(H n0 (le_S_n n n0 H1))))) y)))) x).
 
 theorem blt_lt:
  \forall (x: nat).(\forall (y: nat).((eq bool (blt y x) true) \to (lt y x)))
 \def
- \lambda (x: nat).(nat_ind (\lambda (n: nat).(\forall (y: nat).((eq bool (blt y n) true) \to (lt y n)))) (\lambda (y: nat).(\lambda (H: (eq bool (blt y O) true)).(let H0 \def (match H return (\lambda (_: ?).(\lambda (b: bool).((eq bool b true) \to (lt y O)))) with [refl_equal \Rightarrow (\lambda (H0: (eq bool (blt y O) true)).(let H1 \def (eq_ind bool (blt y O) (\lambda (e: bool).(match e return (\lambda (_: ?).Prop) with [true \Rightarrow False | false \Rightarrow True])) I true H0) in (False_ind (lt y O) H1)))]) in (H0 (refl_equal bool true))))) (\lambda (n: nat).(\lambda (H: ((\forall (y: nat).((eq bool (blt y n) true) \to (lt y n))))).(\lambda (y: nat).(nat_ind (\lambda (n0: nat).((eq bool (blt n0 (S n)) true) \to (lt n0 (S n)))) (\lambda (_: (eq bool true true)).(le_S_n (S O) (S n) (le_n_S (S O) (S n) (le_n_S O n (le_O_n n))))) (\lambda (n0: nat).(\lambda (_: (((eq bool (match n0 with [O \Rightarrow true | (S m) \Rightarrow (blt m n)]) true) \to (lt n0 (S n))))).(\lambda (H1: (eq bool (blt n0 n) true)).(lt_le_S (S n0) (S n) (lt_n_S n0 n (H n0 H1)))))) y)))) x).
+ \lambda (x: nat).(nat_ind (\lambda (n: nat).(\forall (y: nat).((eq bool (blt y n) true) \to (lt y n)))) (\lambda (y: nat).(\lambda (H: (eq bool (blt y O) true)).(let H0 \def (match H return (\lambda (b: bool).(\lambda (_: (eq ? ? b)).((eq bool b true) \to (lt y O)))) with [refl_equal \Rightarrow (\lambda (H0: (eq bool (blt y O) true)).(let H1 \def (eq_ind bool (blt y O) (\lambda (e: bool).(match e return (\lambda (_: ?).Prop) with [true \Rightarrow False | false \Rightarrow True])) I true H0) in (False_ind (lt y O) H1)))]) in (H0 (refl_equal bool true))))) (\lambda (n: nat).(\lambda (H: ((\forall (y: nat).((eq bool (blt y n) true) \to (lt y n))))).(\lambda (y: nat).(nat_ind (\lambda (n0: nat).((eq bool (blt n0 (S n)) true) \to (lt n0 (S n)))) (\lambda (_: (eq bool true true)).(le_S_n (S O) (S n) (le_n_S (S O) (S n) (le_n_S O n (le_O_n n))))) (\lambda (n0: nat).(\lambda (_: (((eq bool (match n0 with [O \Rightarrow true | (S m) \Rightarrow (blt m n)]) true) \to (lt n0 (S n))))).(\lambda (H1: (eq bool (blt n0 n) true)).(lt_le_S (S n0) (S n) (lt_n_S n0 n (H n0 H1)))))) y)))) x).
 
 theorem bge_le:
  \forall (x: nat).(\forall (y: nat).((eq bool (blt y x) false) \to (le x y)))
 \def
- \lambda (x: nat).(nat_ind (\lambda (n: nat).(\forall (y: nat).((eq bool (blt y n) false) \to (le n y)))) (\lambda (y: nat).(\lambda (_: (eq bool (blt y O) false)).(le_O_n y))) (\lambda (n: nat).(\lambda (H: ((\forall (y: nat).((eq bool (blt y n) false) \to (le n y))))).(\lambda (y: nat).(nat_ind (\lambda (n0: nat).((eq bool (blt n0 (S n)) false) \to (le (S n) n0))) (\lambda (H0: (eq bool (blt O (S n)) false)).(let H1 \def (match H0 return (\lambda (_: ?).(\lambda (b: bool).((eq bool b false) \to (le (S n) O)))) with [refl_equal \Rightarrow (\lambda (H1: (eq bool (blt O (S n)) false)).(let H2 \def (eq_ind bool (blt O (S n)) (\lambda (e: bool).(match e return (\lambda (_: ?).Prop) with [true \Rightarrow True | false \Rightarrow False])) I false H1) in (False_ind (le (S n) O) H2)))]) in (H1 (refl_equal bool false)))) (\lambda (n0: nat).(\lambda (_: (((eq bool (blt n0 (S n)) false) \to (le (S n) n0)))).(\lambda (H1: (eq bool (blt (S n0) (S n)) false)).(le_S_n (S n) (S n0) (le_n_S (S n) (S n0) (le_n_S n n0 (H n0 H1))))))) y)))) x).
+ \lambda (x: nat).(nat_ind (\lambda (n: nat).(\forall (y: nat).((eq bool (blt y n) false) \to (le n y)))) (\lambda (y: nat).(\lambda (_: (eq bool (blt y O) false)).(le_O_n y))) (\lambda (n: nat).(\lambda (H: ((\forall (y: nat).((eq bool (blt y n) false) \to (le n y))))).(\lambda (y: nat).(nat_ind (\lambda (n0: nat).((eq bool (blt n0 (S n)) false) \to (le (S n) n0))) (\lambda (H0: (eq bool (blt O (S n)) false)).(let H1 \def (match H0 return (\lambda (b: bool).(\lambda (_: (eq ? ? b)).((eq bool b false) \to (le (S n) O)))) with [refl_equal \Rightarrow (\lambda (H1: (eq bool (blt O (S n)) false)).(let H2 \def (eq_ind bool (blt O (S n)) (\lambda (e: bool).(match e return (\lambda (_: ?).Prop) with [true \Rightarrow True | false \Rightarrow False])) I false H1) in (False_ind (le (S n) O) H2)))]) in (H1 (refl_equal bool false)))) (\lambda (n0: nat).(\lambda (_: (((eq bool (blt n0 (S n)) false) \to (le (S n) n0)))).(\lambda (H1: (eq bool (blt (S n0) (S n)) false)).(le_S_n (S n) (S n0) (le_n_S (S n) (S n0) (le_n_S n n0 (H n0 H1))))))) y)))) x).
 

diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/Preamble.ma b/matita/contribs/LAMBDA-TYPES/Level-1/Preamble.ma
index 2055f18959992b360c9f7364e8476d7fcbbf2918..43cfd87cbaec7a0eb850267a9bea75b66f8306e6 100644 (file)
--- a/matita/contribs/LAMBDA-TYPES/Level-1/Preamble.ma
+++ b/matita/contribs/LAMBDA-TYPES/Level-1/Preamble.ma
@@ -34,7 +34,9 @@ default "false"
 
 default "absurd"
  cic:/Coq/Init/Logic/absurd.con.
-         
+
+interpretation "Coq's leibnitz's equality" 'eq x y = (cic:/Coq/Init/Logic/eq.ind#xpointer(1/1) _ x y).
+interpretation "Coq's not equal to (leibnitz)" 'neq x y = (cic:/Coq/Init/Logic/not.con (cic:/Coq/Init/Logic/eq.ind#xpointer(1/1) _ x y)).
 interpretation "Coq's natural plus" 'plus x y = (cic:/Coq/Init/Peano/plus.con x y).
 interpretation "Coq's natural 'less or equal to'" 'leq x y = (cic:/Coq/Init/Peano/le.ind#xpointer(1/1) x y).
 
@@ -86,3 +88,5 @@ qed.
 theorem plus_le_reg_l: \forall p,n,m. p + n <= p + m \to n <= m.
  intros. apply plus_le_reg_l; auto.
 qed.
+
+definition sym_equal \def sym_eq.