From: Ferruccio Guidi Date: Sun, 10 Sep 2006 10:25:22 +0000 (+0000) Subject: 3 problems solved patching the alpha-conversion of coq 7.3.1 X-Git-Tag: 0.4.95@7852~1059 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=b378364437252c019b50eee17b45847d882c1149;p=helm.git 3 problems solved patching the alpha-conversion of coq 7.3.1 --- diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/drop1/getl.ma b/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/drop1/getl.ma index 879483c42..4adda6f18 100644 --- a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/drop1/getl.ma +++ b/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/drop1/getl.ma @@ -18,12 +18,142 @@ set "baseuri" "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/drop1/getl". include "drop1/defs.ma". -include "getl/defs.ma". +include "getl/drop.ma". -axiom drop1_getl_trans: +theorem drop1_getl_trans: \forall (hds: PList).(\forall (c1: C).(\forall (c2: C).((drop1 hds c2 c1) \to (\forall (b: B).(\forall (e1: C).(\forall (v: T).(\forall (i: nat).((getl i c1 (CHead e1 (Bind b) v)) \to (ex C (\lambda (e2: C).(getl (trans hds i) c2 (CHead e2 (Bind b) (ctrans hds i v))))))))))))) -. +\def + \lambda (hds: PList).(PList_ind (\lambda (p: PList).(\forall (c1: +C).(\forall (c2: C).((drop1 p c2 c1) \to (\forall (b: B).(\forall (e1: +C).(\forall (v: T).(\forall (i: nat).((getl i c1 (CHead e1 (Bind b) v)) \to +(ex C (\lambda (e2: C).(getl (trans p i) c2 (CHead e2 (Bind b) (ctrans p i +v)))))))))))))) (\lambda (c1: C).(\lambda (c2: C).(\lambda (H: (drop1 PNil c2 +c1)).(\lambda (b: B).(\lambda (e1: C).(\lambda (v: T).(\lambda (i: +nat).(\lambda (H0: (getl i c1 (CHead e1 (Bind b) v))).(let H1 \def (match H +in drop1 return (\lambda (p: PList).(\lambda (c: C).(\lambda (c0: C).(\lambda +(_: (drop1 p c c0)).((eq PList p PNil) \to ((eq C c c2) \to ((eq C c0 c1) \to +(ex C (\lambda (e2: C).(getl i c2 (CHead e2 (Bind b) v))))))))))) with +[(drop1_nil c) \Rightarrow (\lambda (_: (eq PList PNil PNil)).(\lambda (H2: +(eq C c c2)).(\lambda (H3: (eq C c c1)).(eq_ind C c2 (\lambda (c0: C).((eq C +c0 c1) \to (ex C (\lambda (e2: C).(getl i c2 (CHead e2 (Bind b) v)))))) +(\lambda (H4: (eq C c2 c1)).(eq_ind C c1 (\lambda (c0: C).(ex C (\lambda (e2: +C).(getl i c0 (CHead e2 (Bind b) v))))) (ex_intro C (\lambda (e2: C).(getl i +c1 (CHead e2 (Bind b) v))) e1 H0) c2 (sym_eq C c2 c1 H4))) c (sym_eq C c c2 +H2) H3)))) | (drop1_cons c0 c3 h d H1 c4 hds0 H2) \Rightarrow (\lambda (H3: +(eq PList (PCons h d hds0) PNil)).(\lambda (H4: (eq C c0 c2)).(\lambda (H5: +(eq C c4 c1)).((let H6 \def (eq_ind PList (PCons h d hds0) (\lambda (e: +PList).(match e in PList return (\lambda (_: PList).Prop) with [PNil +\Rightarrow False | (PCons _ _ _) \Rightarrow True])) I PNil H3) in +(False_ind ((eq C c0 c2) \to ((eq C c4 c1) \to ((drop h d c0 c3) \to ((drop1 +hds0 c3 c4) \to (ex C (\lambda (e2: C).(getl i c2 (CHead e2 (Bind b) +v)))))))) H6)) H4 H5 H1 H2))))]) in (H1 (refl_equal PList PNil) (refl_equal C +c2) (refl_equal C c1))))))))))) (\lambda (h: nat).(\lambda (d: nat).(\lambda +(hds0: PList).(\lambda (H: ((\forall (c1: C).(\forall (c2: C).((drop1 hds0 c2 +c1) \to (\forall (b: B).(\forall (e1: C).(\forall (v: T).(\forall (i: +nat).((getl i c1 (CHead e1 (Bind b) v)) \to (ex C (\lambda (e2: C).(getl +(trans hds0 i) c2 (CHead e2 (Bind b) (ctrans hds0 i v))))))))))))))).(\lambda +(c1: C).(\lambda (c2: C).(\lambda (H0: (drop1 (PCons h d hds0) c2 +c1)).(\lambda (b: B).(\lambda (e1: C).(\lambda (v: T).(\lambda (i: +nat).(\lambda (H1: (getl i c1 (CHead e1 (Bind b) v))).(let H2 \def (match H0 +in drop1 return (\lambda (p: PList).(\lambda (c: C).(\lambda (c0: C).(\lambda +(_: (drop1 p c c0)).((eq PList p (PCons h d hds0)) \to ((eq C c c2) \to ((eq +C c0 c1) \to (ex C (\lambda (e2: C).(getl (match (blt (trans hds0 i) d) with +[true \Rightarrow (trans hds0 i) | false \Rightarrow (plus (trans hds0 i) +h)]) c2 (CHead e2 (Bind b) (match (blt (trans hds0 i) d) with [true +\Rightarrow (lift h (minus d (S (trans hds0 i))) (ctrans hds0 i v)) | false +\Rightarrow (ctrans hds0 i v)])))))))))))) with [(drop1_nil c) \Rightarrow +(\lambda (H2: (eq PList PNil (PCons h d hds0))).(\lambda (H3: (eq C c +c2)).(\lambda (H4: (eq C c c1)).((let H5 \def (eq_ind PList PNil (\lambda (e: +PList).(match e in PList return (\lambda (_: PList).Prop) with [PNil +\Rightarrow True | (PCons _ _ _) \Rightarrow False])) I (PCons h d hds0) H2) +in (False_ind ((eq C c c2) \to ((eq C c c1) \to (ex C (\lambda (e2: C).(getl +(match (blt (trans hds0 i) d) with [true \Rightarrow (trans hds0 i) | false +\Rightarrow (plus (trans hds0 i) h)]) c2 (CHead e2 (Bind b) (match (blt +(trans hds0 i) d) with [true \Rightarrow (lift h (minus d (S (trans hds0 i))) +(ctrans hds0 i v)) | false \Rightarrow (ctrans hds0 i v)]))))))) H5)) H3 +H4)))) | (drop1_cons c0 c3 h0 d0 H2 c4 hds1 H3) \Rightarrow (\lambda (H4: (eq +PList (PCons h0 d0 hds1) (PCons h d hds0))).(\lambda (H5: (eq C c0 +c2)).(\lambda (H6: (eq C c4 c1)).((let H7 \def (f_equal PList PList (\lambda +(e: PList).(match e in PList return (\lambda (_: PList).PList) with [PNil +\Rightarrow hds1 | (PCons _ _ p) \Rightarrow p])) (PCons h0 d0 hds1) (PCons h +d hds0) H4) in ((let H8 \def (f_equal PList nat (\lambda (e: PList).(match e +in PList return (\lambda (_: PList).nat) with [PNil \Rightarrow d0 | (PCons _ +n _) \Rightarrow n])) (PCons h0 d0 hds1) (PCons h d hds0) H4) in ((let H9 +\def (f_equal PList nat (\lambda (e: PList).(match e in PList return (\lambda +(_: PList).nat) with [PNil \Rightarrow h0 | (PCons n _ _) \Rightarrow n])) +(PCons h0 d0 hds1) (PCons h d hds0) H4) in (eq_ind nat h (\lambda (n: +nat).((eq nat d0 d) \to ((eq PList hds1 hds0) \to ((eq C c0 c2) \to ((eq C c4 +c1) \to ((drop n d0 c0 c3) \to ((drop1 hds1 c3 c4) \to (ex C (\lambda (e2: +C).(getl (match (blt (trans hds0 i) d) with [true \Rightarrow (trans hds0 i) +| false \Rightarrow (plus (trans hds0 i) h)]) c2 (CHead e2 (Bind b) (match +(blt (trans hds0 i) d) with [true \Rightarrow (lift h (minus d (S (trans hds0 +i))) (ctrans hds0 i v)) | false \Rightarrow (ctrans hds0 i v)])))))))))))) +(\lambda (H10: (eq nat d0 d)).(eq_ind nat d (\lambda (n: nat).((eq PList hds1 +hds0) \to ((eq C c0 c2) \to ((eq C c4 c1) \to ((drop h n c0 c3) \to ((drop1 +hds1 c3 c4) \to (ex C (\lambda (e2: C).(getl (match (blt (trans hds0 i) d) +with [true \Rightarrow (trans hds0 i) | false \Rightarrow (plus (trans hds0 +i) h)]) c2 (CHead e2 (Bind b) (match (blt (trans hds0 i) d) with [true +\Rightarrow (lift h (minus d (S (trans hds0 i))) (ctrans hds0 i v)) | false +\Rightarrow (ctrans hds0 i v)]))))))))))) (\lambda (H11: (eq PList hds1 +hds0)).(eq_ind PList hds0 (\lambda (p: PList).((eq C c0 c2) \to ((eq C c4 c1) +\to ((drop h d c0 c3) \to ((drop1 p c3 c4) \to (ex C (\lambda (e2: C).(getl +(match (blt (trans hds0 i) d) with [true \Rightarrow (trans hds0 i) | false +\Rightarrow (plus (trans hds0 i) h)]) c2 (CHead e2 (Bind b) (match (blt +(trans hds0 i) d) with [true \Rightarrow (lift h (minus d (S (trans hds0 i))) +(ctrans hds0 i v)) | false \Rightarrow (ctrans hds0 i v)])))))))))) (\lambda +(H12: (eq C c0 c2)).(eq_ind C c2 (\lambda (c: C).((eq C c4 c1) \to ((drop h d +c c3) \to ((drop1 hds0 c3 c4) \to (ex C (\lambda (e2: C).(getl (match (blt +(trans hds0 i) d) with [true \Rightarrow (trans hds0 i) | false \Rightarrow +(plus (trans hds0 i) h)]) c2 (CHead e2 (Bind b) (match (blt (trans hds0 i) d) +with [true \Rightarrow (lift h (minus d (S (trans hds0 i))) (ctrans hds0 i +v)) | false \Rightarrow (ctrans hds0 i v)]))))))))) (\lambda (H13: (eq C c4 +c1)).(eq_ind C c1 (\lambda (c: C).((drop h d c2 c3) \to ((drop1 hds0 c3 c) +\to (ex C (\lambda (e2: C).(getl (match (blt (trans hds0 i) d) with [true +\Rightarrow (trans hds0 i) | false \Rightarrow (plus (trans hds0 i) h)]) c2 +(CHead e2 (Bind b) (match (blt (trans hds0 i) d) with [true \Rightarrow (lift +h (minus d (S (trans hds0 i))) (ctrans hds0 i v)) | false \Rightarrow (ctrans +hds0 i v)])))))))) (\lambda (H14: (drop h d c2 c3)).(\lambda (H15: (drop1 +hds0 c3 c1)).(xinduction bool (blt (trans hds0 i) d) (\lambda (b0: bool).(ex +C (\lambda (e2: C).(getl (match b0 with [true \Rightarrow (trans hds0 i) | +false \Rightarrow (plus (trans hds0 i) h)]) c2 (CHead e2 (Bind b) (match b0 +with [true \Rightarrow (lift h (minus d (S (trans hds0 i))) (ctrans hds0 i +v)) | false \Rightarrow (ctrans hds0 i v)])))))) (\lambda (x_x: +bool).(bool_ind (\lambda (b0: bool).((eq bool (blt (trans hds0 i) d) b0) \to +(ex C (\lambda (e2: C).(getl (match b0 with [true \Rightarrow (trans hds0 i) +| false \Rightarrow (plus (trans hds0 i) h)]) c2 (CHead e2 (Bind b) (match b0 +with [true \Rightarrow (lift h (minus d (S (trans hds0 i))) (ctrans hds0 i +v)) | false \Rightarrow (ctrans hds0 i v)]))))))) (\lambda (H16: (eq bool +(blt (trans hds0 i) d) true)).(let H_x \def (H c1 c3 H15 b e1 v i H1) in (let +H17 \def H_x in (ex_ind C (\lambda (e2: C).(getl (trans hds0 i) c3 (CHead e2 +(Bind b) (ctrans hds0 i v)))) (ex C (\lambda (e2: C).(getl (trans hds0 i) c2 +(CHead e2 (Bind b) (lift h (minus d (S (trans hds0 i))) (ctrans hds0 i +v)))))) (\lambda (x: C).(\lambda (H18: (getl (trans hds0 i) c3 (CHead x (Bind +b) (ctrans hds0 i v)))).(let H_x0 \def (drop_getl_trans_lt (trans hds0 i) d +(le_S_n (S (trans hds0 i)) d (lt_le_S (S (trans hds0 i)) (S d) (blt_lt (S d) +(S (trans hds0 i)) H16))) c2 c3 h H14 b x (ctrans hds0 i v) H18) in (let H19 +\def H_x0 in (ex2_ind C (\lambda (e2: C).(getl (trans hds0 i) c2 (CHead e2 +(Bind b) (lift h (minus d (S (trans hds0 i))) (ctrans hds0 i v))))) (\lambda +(e2: C).(drop h (minus d (S (trans hds0 i))) e2 x)) (ex C (\lambda (e2: +C).(getl (trans hds0 i) c2 (CHead e2 (Bind b) (lift h (minus d (S (trans hds0 +i))) (ctrans hds0 i v)))))) (\lambda (x0: C).(\lambda (H20: (getl (trans hds0 +i) c2 (CHead x0 (Bind b) (lift h (minus d (S (trans hds0 i))) (ctrans hds0 i +v))))).(\lambda (_: (drop h (minus d (S (trans hds0 i))) x0 x)).(ex_intro C +(\lambda (e2: C).(getl (trans hds0 i) c2 (CHead e2 (Bind b) (lift h (minus d +(S (trans hds0 i))) (ctrans hds0 i v))))) x0 H20)))) H19))))) H17)))) +(\lambda (H16: (eq bool (blt (trans hds0 i) d) false)).(let H_x \def (H c1 c3 +H15 b e1 v i H1) in (let H17 \def H_x in (ex_ind C (\lambda (e2: C).(getl +(trans hds0 i) c3 (CHead e2 (Bind b) (ctrans hds0 i v)))) (ex C (\lambda (e2: +C).(getl (plus (trans hds0 i) h) c2 (CHead e2 (Bind b) (ctrans hds0 i v))))) +(\lambda (x: C).(\lambda (H18: (getl (trans hds0 i) c3 (CHead x (Bind b) +(ctrans hds0 i v)))).(let H19 \def (drop_getl_trans_ge (trans hds0 i) c2 c3 d +h H14 (CHead x (Bind b) (ctrans hds0 i v)) H18) in (ex_intro C (\lambda (e2: +C).(getl (plus (trans hds0 i) h) c2 (CHead e2 (Bind b) (ctrans hds0 i v)))) x +(H19 (bge_le d (trans hds0 i) H16)))))) H17)))) x_x))))) c4 (sym_eq C c4 c1 +H13))) c0 (sym_eq C c0 c2 H12))) hds1 (sym_eq PList hds1 hds0 H11))) d0 +(sym_eq nat d0 d H10))) h0 (sym_eq nat h0 h H9))) H8)) H7)) H5 H6 H2 H3))))]) +in (H2 (refl_equal PList (PCons h d hds0)) (refl_equal C c2) (refl_equal C +c1))))))))))))))) hds). diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/iso/props.ma b/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/iso/props.ma index c6cd772d2..817e15f80 100644 --- a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/iso/props.ma +++ b/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/iso/props.ma @@ -18,8 +18,90 @@ set "baseuri" "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/iso/props". include "iso/defs.ma". -axiom iso_trans: +theorem iso_trans: \forall (t1: T).(\forall (t2: T).((iso t1 t2) \to (\forall (t3: T).((iso t2 t3) \to (iso t1 t3))))) -. +\def + \lambda (t1: T).(\lambda (t2: T).(\lambda (H: (iso t1 t2)).(iso_ind (\lambda +(t: T).(\lambda (t0: T).(\forall (t3: T).((iso t0 t3) \to (iso t t3))))) +(\lambda (n1: nat).(\lambda (n2: nat).(\lambda (t3: T).(\lambda (H0: (iso +(TSort n2) t3)).(let H1 \def (match H0 in iso return (\lambda (t: T).(\lambda +(t0: T).(\lambda (_: (iso t t0)).((eq T t (TSort n2)) \to ((eq T t0 t3) \to +(iso (TSort n1) t3)))))) with [(iso_sort n0 n3) \Rightarrow (\lambda (H1: (eq +T (TSort n0) (TSort n2))).(\lambda (H2: (eq T (TSort n3) t3)).((let H3 \def +(f_equal T nat (\lambda (e: T).(match e in T return (\lambda (_: T).nat) with +[(TSort n) \Rightarrow n | (TLRef _) \Rightarrow n0 | (THead _ _ _) +\Rightarrow n0])) (TSort n0) (TSort n2) H1) in (eq_ind nat n2 (\lambda (_: +nat).((eq T (TSort n3) t3) \to (iso (TSort n1) t3))) (\lambda (H4: (eq T +(TSort n3) t3)).(eq_ind T (TSort n3) (\lambda (t: T).(iso (TSort n1) t)) +(iso_sort n1 n3) t3 H4)) n0 (sym_eq nat n0 n2 H3))) H2))) | (iso_lref i1 i2) +\Rightarrow (\lambda (H1: (eq T (TLRef i1) (TSort n2))).(\lambda (H2: (eq T +(TLRef i2) t3)).((let H3 \def (eq_ind T (TLRef i1) (\lambda (e: T).(match e +in T return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef +_) \Rightarrow True | (THead _ _ _) \Rightarrow False])) I (TSort n2) H1) in +(False_ind ((eq T (TLRef i2) t3) \to (iso (TSort n1) t3)) H3)) H2))) | +(iso_head k v1 v2 t0 t4) \Rightarrow (\lambda (H1: (eq T (THead k v1 t0) +(TSort n2))).(\lambda (H2: (eq T (THead k v2 t4) t3)).((let H3 \def (eq_ind T +(THead k v1 t0) (\lambda (e: T).(match e in T return (\lambda (_: T).Prop) +with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow False | (THead _ _ +_) \Rightarrow True])) I (TSort n2) H1) in (False_ind ((eq T (THead k v2 t4) +t3) \to (iso (TSort n1) t3)) H3)) H2)))]) in (H1 (refl_equal T (TSort n2)) +(refl_equal T t3))))))) (\lambda (i1: nat).(\lambda (i2: nat).(\lambda (t3: +T).(\lambda (H0: (iso (TLRef i2) t3)).(let H1 \def (match H0 in iso return +(\lambda (t: T).(\lambda (t0: T).(\lambda (_: (iso t t0)).((eq T t (TLRef +i2)) \to ((eq T t0 t3) \to (iso (TLRef i1) t3)))))) with [(iso_sort n1 n2) +\Rightarrow (\lambda (H1: (eq T (TSort n1) (TLRef i2))).(\lambda (H2: (eq T +(TSort n2) t3)).((let H3 \def (eq_ind T (TSort n1) (\lambda (e: T).(match e +in T return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow True | (TLRef +_) \Rightarrow False | (THead _ _ _) \Rightarrow False])) I (TLRef i2) H1) in +(False_ind ((eq T (TSort n2) t3) \to (iso (TLRef i1) t3)) H3)) H2))) | +(iso_lref i0 i3) \Rightarrow (\lambda (H1: (eq T (TLRef i0) (TLRef +i2))).(\lambda (H2: (eq T (TLRef i3) t3)).((let H3 \def (f_equal T nat +(\lambda (e: T).(match e in T return (\lambda (_: T).nat) with [(TSort _) +\Rightarrow i0 | (TLRef n) \Rightarrow n | (THead _ _ _) \Rightarrow i0])) +(TLRef i0) (TLRef i2) H1) in (eq_ind nat i2 (\lambda (_: nat).((eq T (TLRef +i3) t3) \to (iso (TLRef i1) t3))) (\lambda (H4: (eq T (TLRef i3) t3)).(eq_ind +T (TLRef i3) (\lambda (t: T).(iso (TLRef i1) t)) (iso_lref i1 i3) t3 H4)) i0 +(sym_eq nat i0 i2 H3))) H2))) | (iso_head k v1 v2 t0 t4) \Rightarrow (\lambda +(H1: (eq T (THead k v1 t0) (TLRef i2))).(\lambda (H2: (eq T (THead k v2 t4) +t3)).((let H3 \def (eq_ind T (THead k v1 t0) (\lambda (e: T).(match e in T +return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef _) +\Rightarrow False | (THead _ _ _) \Rightarrow True])) I (TLRef i2) H1) in +(False_ind ((eq T (THead k v2 t4) t3) \to (iso (TLRef i1) t3)) H3)) H2)))]) +in (H1 (refl_equal T (TLRef i2)) (refl_equal T t3))))))) (\lambda (k: +K).(\lambda (v1: T).(\lambda (v2: T).(\lambda (t3: T).(\lambda (t4: +T).(\lambda (t5: T).(\lambda (H0: (iso (THead k v2 t4) t5)).(let H1 \def +(match H0 in iso return (\lambda (t: T).(\lambda (t0: T).(\lambda (_: (iso t +t0)).((eq T t (THead k v2 t4)) \to ((eq T t0 t5) \to (iso (THead k v1 t3) +t5)))))) with [(iso_sort n1 n2) \Rightarrow (\lambda (H1: (eq T (TSort n1) +(THead k v2 t4))).(\lambda (H2: (eq T (TSort n2) t5)).((let H3 \def (eq_ind T +(TSort n1) (\lambda (e: T).(match e in T return (\lambda (_: T).Prop) with +[(TSort _) \Rightarrow True | (TLRef _) \Rightarrow False | (THead _ _ _) +\Rightarrow False])) I (THead k v2 t4) H1) in (False_ind ((eq T (TSort n2) +t5) \to (iso (THead k v1 t3) t5)) H3)) H2))) | (iso_lref i1 i2) \Rightarrow +(\lambda (H1: (eq T (TLRef i1) (THead k v2 t4))).(\lambda (H2: (eq T (TLRef +i2) t5)).((let H3 \def (eq_ind T (TLRef i1) (\lambda (e: T).(match e in T +return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef _) +\Rightarrow True | (THead _ _ _) \Rightarrow False])) I (THead k v2 t4) H1) +in (False_ind ((eq T (TLRef i2) t5) \to (iso (THead k v1 t3) t5)) H3)) H2))) +| (iso_head k0 v0 v3 t0 t6) \Rightarrow (\lambda (H1: (eq T (THead k0 v0 t0) +(THead k v2 t4))).(\lambda (H2: (eq T (THead k0 v3 t6) t5)).((let H3 \def +(f_equal T T (\lambda (e: T).(match e in T return (\lambda (_: T).T) with +[(TSort _) \Rightarrow t0 | (TLRef _) \Rightarrow t0 | (THead _ _ t) +\Rightarrow t])) (THead k0 v0 t0) (THead k v2 t4) H1) in ((let H4 \def +(f_equal T T (\lambda (e: T).(match e in T return (\lambda (_: T).T) with +[(TSort _) \Rightarrow v0 | (TLRef _) \Rightarrow v0 | (THead _ t _) +\Rightarrow t])) (THead k0 v0 t0) (THead k v2 t4) H1) in ((let H5 \def +(f_equal T K (\lambda (e: T).(match e in T return (\lambda (_: T).K) with +[(TSort _) \Rightarrow k0 | (TLRef _) \Rightarrow k0 | (THead k1 _ _) +\Rightarrow k1])) (THead k0 v0 t0) (THead k v2 t4) H1) in (eq_ind K k +(\lambda (k1: K).((eq T v0 v2) \to ((eq T t0 t4) \to ((eq T (THead k1 v3 t6) +t5) \to (iso (THead k v1 t3) t5))))) (\lambda (H6: (eq T v0 v2)).(eq_ind T v2 +(\lambda (_: T).((eq T t0 t4) \to ((eq T (THead k v3 t6) t5) \to (iso (THead +k v1 t3) t5)))) (\lambda (H7: (eq T t0 t4)).(eq_ind T t4 (\lambda (_: T).((eq +T (THead k v3 t6) t5) \to (iso (THead k v1 t3) t5))) (\lambda (H8: (eq T +(THead k v3 t6) t5)).(eq_ind T (THead k v3 t6) (\lambda (t: T).(iso (THead k +v1 t3) t)) (iso_head k v1 v3 t3 t6) t5 H8)) t0 (sym_eq T t0 t4 H7))) v0 +(sym_eq T v0 v2 H6))) k0 (sym_eq K k0 k H5))) H4)) H3)) H2)))]) in (H1 +(refl_equal T (THead k v2 t4)) (refl_equal T t5)))))))))) t1 t2 H))). diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/leq/asucc.ma b/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/leq/asucc.ma index 290c32cc9..079e5c2db 100644 --- a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/leq/asucc.ma +++ b/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/leq/asucc.ma @@ -16,7 +16,7 @@ set "baseuri" "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/leq/asucc". -include "leq/defs.ma". +include "leq/props.ma". include "aplus/props.ma". @@ -81,8 +81,629 @@ a3) (asucc g a4))).(\lambda (a5: A).(\lambda (a6: A).(\lambda (_: (leq g a5 a6)).(\lambda (H3: (leq g (asucc g a5) (asucc g a6))).(leq_head g a3 a4 H0 (asucc g a5) (asucc g a6) H3))))))))) a1 a2 H)))). -axiom asucc_inj: +theorem asucc_inj: \forall (g: G).(\forall (a1: A).(\forall (a2: A).((leq g (asucc g a1) (asucc g a2)) \to (leq g a1 a2)))) -. +\def + \lambda (g: G).(\lambda (a1: A).(A_ind (\lambda (a: A).(\forall (a2: +A).((leq g (asucc g a) (asucc g a2)) \to (leq g a a2)))) (\lambda (n: +nat).(\lambda (n0: nat).(\lambda (a2: A).(A_ind (\lambda (a: A).((leq g +(asucc g (ASort n n0)) (asucc g a)) \to (leq g (ASort n n0) a))) (\lambda +(n1: nat).(\lambda (n2: nat).(\lambda (H: (leq g (asucc g (ASort n n0)) +(asucc g (ASort n1 n2)))).((match n in nat return (\lambda (n3: nat).((leq g +(asucc g (ASort n3 n0)) (asucc g (ASort n1 n2))) \to (leq g (ASort n3 n0) +(ASort n1 n2)))) with [O \Rightarrow (\lambda (H0: (leq g (asucc g (ASort O +n0)) (asucc g (ASort n1 n2)))).((match n1 in nat return (\lambda (n3: +nat).((leq g (asucc g (ASort O n0)) (asucc g (ASort n3 n2))) \to (leq g +(ASort O n0) (ASort n3 n2)))) with [O \Rightarrow (\lambda (H1: (leq g (asucc +g (ASort O n0)) (asucc g (ASort O n2)))).(let H2 \def (match H1 in leq return +(\lambda (a: A).(\lambda (a0: A).(\lambda (_: (leq ? a a0)).((eq A a (ASort O +(next g n0))) \to ((eq A a0 (ASort O (next g n2))) \to (leq g (ASort O n0) +(ASort O n2))))))) with [(leq_sort h1 h2 n3 n4 k H2) \Rightarrow (\lambda +(H3: (eq A (ASort h1 n3) (ASort O (next g n0)))).(\lambda (H4: (eq A (ASort +h2 n4) (ASort O (next g n2)))).((let H5 \def (f_equal A nat (\lambda (e: +A).(match e in A return (\lambda (_: A).nat) with [(ASort _ n5) \Rightarrow +n5 | (AHead _ _) \Rightarrow n3])) (ASort h1 n3) (ASort O (next g n0)) H3) in +((let H6 \def (f_equal A nat (\lambda (e: A).(match e in A return (\lambda +(_: A).nat) with [(ASort n5 _) \Rightarrow n5 | (AHead _ _) \Rightarrow h1])) +(ASort h1 n3) (ASort O (next g n0)) H3) in (eq_ind nat O (\lambda (n5: +nat).((eq nat n3 (next g n0)) \to ((eq A (ASort h2 n4) (ASort O (next g n2))) +\to ((eq A (aplus g (ASort n5 n3) k) (aplus g (ASort h2 n4) k)) \to (leq g +(ASort O n0) (ASort O n2)))))) (\lambda (H7: (eq nat n3 (next g n0))).(eq_ind +nat (next g n0) (\lambda (n5: nat).((eq A (ASort h2 n4) (ASort O (next g +n2))) \to ((eq A (aplus g (ASort O n5) k) (aplus g (ASort h2 n4) k)) \to (leq +g (ASort O n0) (ASort O n2))))) (\lambda (H8: (eq A (ASort h2 n4) (ASort O +(next g n2)))).(let H9 \def (f_equal A nat (\lambda (e: A).(match e in A +return (\lambda (_: A).nat) with [(ASort _ n5) \Rightarrow n5 | (AHead _ _) +\Rightarrow n4])) (ASort h2 n4) (ASort O (next g n2)) H8) in ((let H10 \def +(f_equal A nat (\lambda (e: A).(match e in A return (\lambda (_: A).nat) with +[(ASort n5 _) \Rightarrow n5 | (AHead _ _) \Rightarrow h2])) (ASort h2 n4) +(ASort O (next g n2)) H8) in (eq_ind nat O (\lambda (n5: nat).((eq nat n4 +(next g n2)) \to ((eq A (aplus g (ASort O (next g n0)) k) (aplus g (ASort n5 +n4) k)) \to (leq g (ASort O n0) (ASort O n2))))) (\lambda (H11: (eq nat n4 +(next g n2))).(eq_ind nat (next g n2) (\lambda (n5: nat).((eq A (aplus g +(ASort O (next g n0)) k) (aplus g (ASort O n5) k)) \to (leq g (ASort O n0) +(ASort O n2)))) (\lambda (H12: (eq A (aplus g (ASort O (next g n0)) k) (aplus +g (ASort O (next g n2)) k))).(let H13 \def (eq_ind_r A (aplus g (ASort O +(next g n0)) k) (\lambda (a: A).(eq A a (aplus g (ASort O (next g n2)) k))) +H12 (aplus g (ASort O n0) (S k)) (aplus_sort_O_S_simpl g n0 k)) in (let H14 +\def (eq_ind_r A (aplus g (ASort O (next g n2)) k) (\lambda (a: A).(eq A +(aplus g (ASort O n0) (S k)) a)) H13 (aplus g (ASort O n2) (S k)) +(aplus_sort_O_S_simpl g n2 k)) in (leq_sort g O O n0 n2 (S k) H14)))) n4 +(sym_eq nat n4 (next g n2) H11))) h2 (sym_eq nat h2 O H10))) H9))) n3 (sym_eq +nat n3 (next g n0) H7))) h1 (sym_eq nat h1 O H6))) H5)) H4 H2))) | (leq_head +a0 a3 H2 a4 a5 H3) \Rightarrow (\lambda (H4: (eq A (AHead a0 a4) (ASort O +(next g n0)))).(\lambda (H5: (eq A (AHead a3 a5) (ASort O (next g +n2)))).((let H6 \def (eq_ind A (AHead a0 a4) (\lambda (e: A).(match e in A +return (\lambda (_: A).Prop) with [(ASort _ _) \Rightarrow False | (AHead _ +_) \Rightarrow True])) I (ASort O (next g n0)) H4) in (False_ind ((eq A +(AHead a3 a5) (ASort O (next g n2))) \to ((leq g a0 a3) \to ((leq g a4 a5) +\to (leq g (ASort O n0) (ASort O n2))))) H6)) H5 H2 H3)))]) in (H2 +(refl_equal A (ASort O (next g n0))) (refl_equal A (ASort O (next g n2)))))) +| (S n3) \Rightarrow (\lambda (H1: (leq g (asucc g (ASort O n0)) (asucc g +(ASort (S n3) n2)))).(let H2 \def (match H1 in leq return (\lambda (a: +A).(\lambda (a0: A).(\lambda (_: (leq ? a a0)).((eq A a (ASort O (next g +n0))) \to ((eq A a0 (ASort n3 n2)) \to (leq g (ASort O n0) (ASort (S n3) +n2))))))) with [(leq_sort h1 h2 n4 n5 k H2) \Rightarrow (\lambda (H3: (eq A +(ASort h1 n4) (ASort O (next g n0)))).(\lambda (H4: (eq A (ASort h2 n5) +(ASort n3 n2))).((let H5 \def (f_equal A nat (\lambda (e: A).(match e in A +return (\lambda (_: A).nat) with [(ASort _ n6) \Rightarrow n6 | (AHead _ _) +\Rightarrow n4])) (ASort h1 n4) (ASort O (next g n0)) H3) in ((let H6 \def +(f_equal A nat (\lambda (e: A).(match e in A return (\lambda (_: A).nat) with +[(ASort n6 _) \Rightarrow n6 | (AHead _ _) \Rightarrow h1])) (ASort h1 n4) +(ASort O (next g n0)) H3) in (eq_ind nat O (\lambda (n6: nat).((eq nat n4 +(next g n0)) \to ((eq A (ASort h2 n5) (ASort n3 n2)) \to ((eq A (aplus g +(ASort n6 n4) k) (aplus g (ASort h2 n5) k)) \to (leq g (ASort O n0) (ASort (S +n3) n2)))))) (\lambda (H7: (eq nat n4 (next g n0))).(eq_ind nat (next g n0) +(\lambda (n6: nat).((eq A (ASort h2 n5) (ASort n3 n2)) \to ((eq A (aplus g +(ASort O n6) k) (aplus g (ASort h2 n5) k)) \to (leq g (ASort O n0) (ASort (S +n3) n2))))) (\lambda (H8: (eq A (ASort h2 n5) (ASort n3 n2))).(let H9 \def +(f_equal A nat (\lambda (e: A).(match e in A return (\lambda (_: A).nat) with +[(ASort _ n6) \Rightarrow n6 | (AHead _ _) \Rightarrow n5])) (ASort h2 n5) +(ASort n3 n2) H8) in ((let H10 \def (f_equal A nat (\lambda (e: A).(match e +in A return (\lambda (_: A).nat) with [(ASort n6 _) \Rightarrow n6 | (AHead _ +_) \Rightarrow h2])) (ASort h2 n5) (ASort n3 n2) H8) in (eq_ind nat n3 +(\lambda (n6: nat).((eq nat n5 n2) \to ((eq A (aplus g (ASort O (next g n0)) +k) (aplus g (ASort n6 n5) k)) \to (leq g (ASort O n0) (ASort (S n3) n2))))) +(\lambda (H11: (eq nat n5 n2)).(eq_ind nat n2 (\lambda (n6: nat).((eq A +(aplus g (ASort O (next g n0)) k) (aplus g (ASort n3 n6) k)) \to (leq g +(ASort O n0) (ASort (S n3) n2)))) (\lambda (H12: (eq A (aplus g (ASort O +(next g n0)) k) (aplus g (ASort n3 n2) k))).(let H13 \def (eq_ind_r A (aplus +g (ASort O (next g n0)) k) (\lambda (a: A).(eq A a (aplus g (ASort n3 n2) +k))) H12 (aplus g (ASort O n0) (S k)) (aplus_sort_O_S_simpl g n0 k)) in (let +H14 \def (eq_ind_r A (aplus g (ASort n3 n2) k) (\lambda (a: A).(eq A (aplus g +(ASort O n0) (S k)) a)) H13 (aplus g (ASort (S n3) n2) (S k)) +(aplus_sort_S_S_simpl g n2 n3 k)) in (leq_sort g O (S n3) n0 n2 (S k) H14)))) +n5 (sym_eq nat n5 n2 H11))) h2 (sym_eq nat h2 n3 H10))) H9))) n4 (sym_eq nat +n4 (next g n0) H7))) h1 (sym_eq nat h1 O H6))) H5)) H4 H2))) | (leq_head a0 +a3 H2 a4 a5 H3) \Rightarrow (\lambda (H4: (eq A (AHead a0 a4) (ASort O (next +g n0)))).(\lambda (H5: (eq A (AHead a3 a5) (ASort n3 n2))).((let H6 \def +(eq_ind A (AHead a0 a4) (\lambda (e: A).(match e in A return (\lambda (_: +A).Prop) with [(ASort _ _) \Rightarrow False | (AHead _ _) \Rightarrow +True])) I (ASort O (next g n0)) H4) in (False_ind ((eq A (AHead a3 a5) (ASort +n3 n2)) \to ((leq g a0 a3) \to ((leq g a4 a5) \to (leq g (ASort O n0) (ASort +(S n3) n2))))) H6)) H5 H2 H3)))]) in (H2 (refl_equal A (ASort O (next g n0))) +(refl_equal A (ASort n3 n2)))))]) H0)) | (S n3) \Rightarrow (\lambda (H0: +(leq g (asucc g (ASort (S n3) n0)) (asucc g (ASort n1 n2)))).((match n1 in +nat return (\lambda (n4: nat).((leq g (asucc g (ASort (S n3) n0)) (asucc g +(ASort n4 n2))) \to (leq g (ASort (S n3) n0) (ASort n4 n2)))) with [O +\Rightarrow (\lambda (H1: (leq g (asucc g (ASort (S n3) n0)) (asucc g (ASort +O n2)))).(let H2 \def (match H1 in leq return (\lambda (a: A).(\lambda (a0: +A).(\lambda (_: (leq ? a a0)).((eq A a (ASort n3 n0)) \to ((eq A a0 (ASort O +(next g n2))) \to (leq g (ASort (S n3) n0) (ASort O n2))))))) with [(leq_sort +h1 h2 n4 n5 k H2) \Rightarrow (\lambda (H3: (eq A (ASort h1 n4) (ASort n3 +n0))).(\lambda (H4: (eq A (ASort h2 n5) (ASort O (next g n2)))).((let H5 \def +(f_equal A nat (\lambda (e: A).(match e in A return (\lambda (_: A).nat) with +[(ASort _ n6) \Rightarrow n6 | (AHead _ _) \Rightarrow n4])) (ASort h1 n4) +(ASort n3 n0) H3) in ((let H6 \def (f_equal A nat (\lambda (e: A).(match e in +A return (\lambda (_: A).nat) with [(ASort n6 _) \Rightarrow n6 | (AHead _ _) +\Rightarrow h1])) (ASort h1 n4) (ASort n3 n0) H3) in (eq_ind nat n3 (\lambda +(n6: nat).((eq nat n4 n0) \to ((eq A (ASort h2 n5) (ASort O (next g n2))) \to +((eq A (aplus g (ASort n6 n4) k) (aplus g (ASort h2 n5) k)) \to (leq g (ASort +(S n3) n0) (ASort O n2)))))) (\lambda (H7: (eq nat n4 n0)).(eq_ind nat n0 +(\lambda (n6: nat).((eq A (ASort h2 n5) (ASort O (next g n2))) \to ((eq A +(aplus g (ASort n3 n6) k) (aplus g (ASort h2 n5) k)) \to (leq g (ASort (S n3) +n0) (ASort O n2))))) (\lambda (H8: (eq A (ASort h2 n5) (ASort O (next g +n2)))).(let H9 \def (f_equal A nat (\lambda (e: A).(match e in A return +(\lambda (_: A).nat) with [(ASort _ n6) \Rightarrow n6 | (AHead _ _) +\Rightarrow n5])) (ASort h2 n5) (ASort O (next g n2)) H8) in ((let H10 \def +(f_equal A nat (\lambda (e: A).(match e in A return (\lambda (_: A).nat) with +[(ASort n6 _) \Rightarrow n6 | (AHead _ _) \Rightarrow h2])) (ASort h2 n5) +(ASort O (next g n2)) H8) in (eq_ind nat O (\lambda (n6: nat).((eq nat n5 +(next g n2)) \to ((eq A (aplus g (ASort n3 n0) k) (aplus g (ASort n6 n5) k)) +\to (leq g (ASort (S n3) n0) (ASort O n2))))) (\lambda (H11: (eq nat n5 (next +g n2))).(eq_ind nat (next g n2) (\lambda (n6: nat).((eq A (aplus g (ASort n3 +n0) k) (aplus g (ASort O n6) k)) \to (leq g (ASort (S n3) n0) (ASort O n2)))) +(\lambda (H12: (eq A (aplus g (ASort n3 n0) k) (aplus g (ASort O (next g n2)) +k))).(let H13 \def (eq_ind_r A (aplus g (ASort n3 n0) k) (\lambda (a: A).(eq +A a (aplus g (ASort O (next g n2)) k))) H12 (aplus g (ASort (S n3) n0) (S k)) +(aplus_sort_S_S_simpl g n0 n3 k)) in (let H14 \def (eq_ind_r A (aplus g +(ASort O (next g n2)) k) (\lambda (a: A).(eq A (aplus g (ASort (S n3) n0) (S +k)) a)) H13 (aplus g (ASort O n2) (S k)) (aplus_sort_O_S_simpl g n2 k)) in +(leq_sort g (S n3) O n0 n2 (S k) H14)))) n5 (sym_eq nat n5 (next g n2) H11))) +h2 (sym_eq nat h2 O H10))) H9))) n4 (sym_eq nat n4 n0 H7))) h1 (sym_eq nat h1 +n3 H6))) H5)) H4 H2))) | (leq_head a0 a3 H2 a4 a5 H3) \Rightarrow (\lambda +(H4: (eq A (AHead a0 a4) (ASort n3 n0))).(\lambda (H5: (eq A (AHead a3 a5) +(ASort O (next g n2)))).((let H6 \def (eq_ind A (AHead a0 a4) (\lambda (e: +A).(match e in A return (\lambda (_: A).Prop) with [(ASort _ _) \Rightarrow +False | (AHead _ _) \Rightarrow True])) I (ASort n3 n0) H4) in (False_ind +((eq A (AHead a3 a5) (ASort O (next g n2))) \to ((leq g a0 a3) \to ((leq g a4 +a5) \to (leq g (ASort (S n3) n0) (ASort O n2))))) H6)) H5 H2 H3)))]) in (H2 +(refl_equal A (ASort n3 n0)) (refl_equal A (ASort O (next g n2)))))) | (S n4) +\Rightarrow (\lambda (H1: (leq g (asucc g (ASort (S n3) n0)) (asucc g (ASort +(S n4) n2)))).(let H2 \def (match H1 in leq return (\lambda (a: A).(\lambda +(a0: A).(\lambda (_: (leq ? a a0)).((eq A a (ASort n3 n0)) \to ((eq A a0 +(ASort n4 n2)) \to (leq g (ASort (S n3) n0) (ASort (S n4) n2))))))) with +[(leq_sort h1 h2 n5 n6 k H2) \Rightarrow (\lambda (H3: (eq A (ASort h1 n5) +(ASort n3 n0))).(\lambda (H4: (eq A (ASort h2 n6) (ASort n4 n2))).((let H5 +\def (f_equal A nat (\lambda (e: A).(match e in A return (\lambda (_: A).nat) +with [(ASort _ n7) \Rightarrow n7 | (AHead _ _) \Rightarrow n5])) (ASort h1 +n5) (ASort n3 n0) H3) in ((let H6 \def (f_equal A nat (\lambda (e: A).(match +e in A return (\lambda (_: A).nat) with [(ASort n7 _) \Rightarrow n7 | (AHead +_ _) \Rightarrow h1])) (ASort h1 n5) (ASort n3 n0) H3) in (eq_ind nat n3 +(\lambda (n7: nat).((eq nat n5 n0) \to ((eq A (ASort h2 n6) (ASort n4 n2)) +\to ((eq A (aplus g (ASort n7 n5) k) (aplus g (ASort h2 n6) k)) \to (leq g +(ASort (S n3) n0) (ASort (S n4) n2)))))) (\lambda (H7: (eq nat n5 +n0)).(eq_ind nat n0 (\lambda (n7: nat).((eq A (ASort h2 n6) (ASort n4 n2)) +\to ((eq A (aplus g (ASort n3 n7) k) (aplus g (ASort h2 n6) k)) \to (leq g +(ASort (S n3) n0) (ASort (S n4) n2))))) (\lambda (H8: (eq A (ASort h2 n6) +(ASort n4 n2))).(let H9 \def (f_equal A nat (\lambda (e: A).(match e in A +return (\lambda (_: A).nat) with [(ASort _ n7) \Rightarrow n7 | (AHead _ _) +\Rightarrow n6])) (ASort h2 n6) (ASort n4 n2) H8) in ((let H10 \def (f_equal +A nat (\lambda (e: A).(match e in A return (\lambda (_: A).nat) with [(ASort +n7 _) \Rightarrow n7 | (AHead _ _) \Rightarrow h2])) (ASort h2 n6) (ASort n4 +n2) H8) in (eq_ind nat n4 (\lambda (n7: nat).((eq nat n6 n2) \to ((eq A +(aplus g (ASort n3 n0) k) (aplus g (ASort n7 n6) k)) \to (leq g (ASort (S n3) +n0) (ASort (S n4) n2))))) (\lambda (H11: (eq nat n6 n2)).(eq_ind nat n2 +(\lambda (n7: nat).((eq A (aplus g (ASort n3 n0) k) (aplus g (ASort n4 n7) +k)) \to (leq g (ASort (S n3) n0) (ASort (S n4) n2)))) (\lambda (H12: (eq A +(aplus g (ASort n3 n0) k) (aplus g (ASort n4 n2) k))).(let H13 \def (eq_ind_r +A (aplus g (ASort n3 n0) k) (\lambda (a: A).(eq A a (aplus g (ASort n4 n2) +k))) H12 (aplus g (ASort (S n3) n0) (S k)) (aplus_sort_S_S_simpl g n0 n3 k)) +in (let H14 \def (eq_ind_r A (aplus g (ASort n4 n2) k) (\lambda (a: A).(eq A +(aplus g (ASort (S n3) n0) (S k)) a)) H13 (aplus g (ASort (S n4) n2) (S k)) +(aplus_sort_S_S_simpl g n2 n4 k)) in (leq_sort g (S n3) (S n4) n0 n2 (S k) +H14)))) n6 (sym_eq nat n6 n2 H11))) h2 (sym_eq nat h2 n4 H10))) H9))) n5 +(sym_eq nat n5 n0 H7))) h1 (sym_eq nat h1 n3 H6))) H5)) H4 H2))) | (leq_head +a0 a3 H2 a4 a5 H3) \Rightarrow (\lambda (H4: (eq A (AHead a0 a4) (ASort n3 +n0))).(\lambda (H5: (eq A (AHead a3 a5) (ASort n4 n2))).((let H6 \def (eq_ind +A (AHead a0 a4) (\lambda (e: A).(match e in A return (\lambda (_: A).Prop) +with [(ASort _ _) \Rightarrow False | (AHead _ _) \Rightarrow True])) I +(ASort n3 n0) H4) in (False_ind ((eq A (AHead a3 a5) (ASort n4 n2)) \to ((leq +g a0 a3) \to ((leq g a4 a5) \to (leq g (ASort (S n3) n0) (ASort (S n4) +n2))))) H6)) H5 H2 H3)))]) in (H2 (refl_equal A (ASort n3 n0)) (refl_equal A +(ASort n4 n2)))))]) H0))]) H)))) (\lambda (a: A).(\lambda (H: (((leq g (asucc +g (ASort n n0)) (asucc g a)) \to (leq g (ASort n n0) a)))).(\lambda (a0: +A).(\lambda (H0: (((leq g (asucc g (ASort n n0)) (asucc g a0)) \to (leq g +(ASort n n0) a0)))).(\lambda (H1: (leq g (asucc g (ASort n n0)) (asucc g +(AHead a a0)))).((match n in nat return (\lambda (n1: nat).((((leq g (asucc g +(ASort n1 n0)) (asucc g a)) \to (leq g (ASort n1 n0) a))) \to ((((leq g +(asucc g (ASort n1 n0)) (asucc g a0)) \to (leq g (ASort n1 n0) a0))) \to +((leq g (asucc g (ASort n1 n0)) (asucc g (AHead a a0))) \to (leq g (ASort n1 +n0) (AHead a a0)))))) with [O \Rightarrow (\lambda (_: (((leq g (asucc g +(ASort O n0)) (asucc g a)) \to (leq g (ASort O n0) a)))).(\lambda (_: (((leq +g (asucc g (ASort O n0)) (asucc g a0)) \to (leq g (ASort O n0) +a0)))).(\lambda (H4: (leq g (asucc g (ASort O n0)) (asucc g (AHead a +a0)))).(let H5 \def (match H4 in leq return (\lambda (a3: A).(\lambda (a4: +A).(\lambda (_: (leq ? a3 a4)).((eq A a3 (ASort O (next g n0))) \to ((eq A a4 +(AHead a (asucc g a0))) \to (leq g (ASort O n0) (AHead a a0))))))) with +[(leq_sort h1 h2 n1 n2 k H5) \Rightarrow (\lambda (H6: (eq A (ASort h1 n1) +(ASort O (next g n0)))).(\lambda (H7: (eq A (ASort h2 n2) (AHead a (asucc g +a0)))).((let H8 \def (f_equal A nat (\lambda (e: A).(match e in A return +(\lambda (_: A).nat) with [(ASort _ n3) \Rightarrow n3 | (AHead _ _) +\Rightarrow n1])) (ASort h1 n1) (ASort O (next g n0)) H6) in ((let H9 \def +(f_equal A nat (\lambda (e: A).(match e in A return (\lambda (_: A).nat) with +[(ASort n3 _) \Rightarrow n3 | (AHead _ _) \Rightarrow h1])) (ASort h1 n1) +(ASort O (next g n0)) H6) in (eq_ind nat O (\lambda (n3: nat).((eq nat n1 +(next g n0)) \to ((eq A (ASort h2 n2) (AHead a (asucc g a0))) \to ((eq A +(aplus g (ASort n3 n1) k) (aplus g (ASort h2 n2) k)) \to (leq g (ASort O n0) +(AHead a a0)))))) (\lambda (H10: (eq nat n1 (next g n0))).(eq_ind nat (next g +n0) (\lambda (n3: nat).((eq A (ASort h2 n2) (AHead a (asucc g a0))) \to ((eq +A (aplus g (ASort O n3) k) (aplus g (ASort h2 n2) k)) \to (leq g (ASort O n0) +(AHead a a0))))) (\lambda (H11: (eq A (ASort h2 n2) (AHead a (asucc g +a0)))).(let H12 \def (eq_ind A (ASort h2 n2) (\lambda (e: A).(match e in A +return (\lambda (_: A).Prop) with [(ASort _ _) \Rightarrow True | (AHead _ _) +\Rightarrow False])) I (AHead a (asucc g a0)) H11) in (False_ind ((eq A +(aplus g (ASort O (next g n0)) k) (aplus g (ASort h2 n2) k)) \to (leq g +(ASort O n0) (AHead a a0))) H12))) n1 (sym_eq nat n1 (next g n0) H10))) h1 +(sym_eq nat h1 O H9))) H8)) H7 H5))) | (leq_head a3 a4 H5 a5 a6 H6) +\Rightarrow (\lambda (H7: (eq A (AHead a3 a5) (ASort O (next g +n0)))).(\lambda (H8: (eq A (AHead a4 a6) (AHead a (asucc g a0)))).((let H9 +\def (eq_ind A (AHead a3 a5) (\lambda (e: A).(match e in A return (\lambda +(_: A).Prop) with [(ASort _ _) \Rightarrow False | (AHead _ _) \Rightarrow +True])) I (ASort O (next g n0)) H7) in (False_ind ((eq A (AHead a4 a6) (AHead +a (asucc g a0))) \to ((leq g a3 a4) \to ((leq g a5 a6) \to (leq g (ASort O +n0) (AHead a a0))))) H9)) H8 H5 H6)))]) in (H5 (refl_equal A (ASort O (next g +n0))) (refl_equal A (AHead a (asucc g a0)))))))) | (S n1) \Rightarrow +(\lambda (_: (((leq g (asucc g (ASort (S n1) n0)) (asucc g a)) \to (leq g +(ASort (S n1) n0) a)))).(\lambda (_: (((leq g (asucc g (ASort (S n1) n0)) +(asucc g a0)) \to (leq g (ASort (S n1) n0) a0)))).(\lambda (H4: (leq g (asucc +g (ASort (S n1) n0)) (asucc g (AHead a a0)))).(let H5 \def (match H4 in leq +return (\lambda (a3: A).(\lambda (a4: A).(\lambda (_: (leq ? a3 a4)).((eq A +a3 (ASort n1 n0)) \to ((eq A a4 (AHead a (asucc g a0))) \to (leq g (ASort (S +n1) n0) (AHead a a0))))))) with [(leq_sort h1 h2 n2 n3 k H5) \Rightarrow +(\lambda (H6: (eq A (ASort h1 n2) (ASort n1 n0))).(\lambda (H7: (eq A (ASort +h2 n3) (AHead a (asucc g a0)))).((let H8 \def (f_equal A nat (\lambda (e: +A).(match e in A return (\lambda (_: A).nat) with [(ASort _ n4) \Rightarrow +n4 | (AHead _ _) \Rightarrow n2])) (ASort h1 n2) (ASort n1 n0) H6) in ((let +H9 \def (f_equal A nat (\lambda (e: A).(match e in A return (\lambda (_: +A).nat) with [(ASort n4 _) \Rightarrow n4 | (AHead _ _) \Rightarrow h1])) +(ASort h1 n2) (ASort n1 n0) H6) in (eq_ind nat n1 (\lambda (n4: nat).((eq nat +n2 n0) \to ((eq A (ASort h2 n3) (AHead a (asucc g a0))) \to ((eq A (aplus g +(ASort n4 n2) k) (aplus g (ASort h2 n3) k)) \to (leq g (ASort (S n1) n0) +(AHead a a0)))))) (\lambda (H10: (eq nat n2 n0)).(eq_ind nat n0 (\lambda (n4: +nat).((eq A (ASort h2 n3) (AHead a (asucc g a0))) \to ((eq A (aplus g (ASort +n1 n4) k) (aplus g (ASort h2 n3) k)) \to (leq g (ASort (S n1) n0) (AHead a +a0))))) (\lambda (H11: (eq A (ASort h2 n3) (AHead a (asucc g a0)))).(let H12 +\def (eq_ind A (ASort h2 n3) (\lambda (e: A).(match e in A return (\lambda +(_: A).Prop) with [(ASort _ _) \Rightarrow True | (AHead _ _) \Rightarrow +False])) I (AHead a (asucc g a0)) H11) in (False_ind ((eq A (aplus g (ASort +n1 n0) k) (aplus g (ASort h2 n3) k)) \to (leq g (ASort (S n1) n0) (AHead a +a0))) H12))) n2 (sym_eq nat n2 n0 H10))) h1 (sym_eq nat h1 n1 H9))) H8)) H7 +H5))) | (leq_head a3 a4 H5 a5 a6 H6) \Rightarrow (\lambda (H7: (eq A (AHead +a3 a5) (ASort n1 n0))).(\lambda (H8: (eq A (AHead a4 a6) (AHead a (asucc g +a0)))).((let H9 \def (eq_ind A (AHead a3 a5) (\lambda (e: A).(match e in A +return (\lambda (_: A).Prop) with [(ASort _ _) \Rightarrow False | (AHead _ +_) \Rightarrow True])) I (ASort n1 n0) H7) in (False_ind ((eq A (AHead a4 a6) +(AHead a (asucc g a0))) \to ((leq g a3 a4) \to ((leq g a5 a6) \to (leq g +(ASort (S n1) n0) (AHead a a0))))) H9)) H8 H5 H6)))]) in (H5 (refl_equal A +(ASort n1 n0)) (refl_equal A (AHead a (asucc g a0))))))))]) H H0 H1)))))) +a2)))) (\lambda (a: A).(\lambda (_: ((\forall (a2: A).((leq g (asucc g a) +(asucc g a2)) \to (leq g a a2))))).(\lambda (a0: A).(\lambda (H0: ((\forall +(a2: A).((leq g (asucc g a0) (asucc g a2)) \to (leq g a0 a2))))).(\lambda +(a2: A).(A_ind (\lambda (a3: A).((leq g (asucc g (AHead a a0)) (asucc g a3)) +\to (leq g (AHead a a0) a3))) (\lambda (n: nat).(\lambda (n0: nat).(\lambda +(H1: (leq g (asucc g (AHead a a0)) (asucc g (ASort n n0)))).((match n in nat +return (\lambda (n1: nat).((leq g (asucc g (AHead a a0)) (asucc g (ASort n1 +n0))) \to (leq g (AHead a a0) (ASort n1 n0)))) with [O \Rightarrow (\lambda +(H2: (leq g (asucc g (AHead a a0)) (asucc g (ASort O n0)))).(let H3 \def +(match H2 in leq return (\lambda (a3: A).(\lambda (a4: A).(\lambda (_: (leq ? +a3 a4)).((eq A a3 (AHead a (asucc g a0))) \to ((eq A a4 (ASort O (next g +n0))) \to (leq g (AHead a a0) (ASort O n0))))))) with [(leq_sort h1 h2 n1 n2 +k H3) \Rightarrow (\lambda (H4: (eq A (ASort h1 n1) (AHead a (asucc g +a0)))).(\lambda (H5: (eq A (ASort h2 n2) (ASort O (next g n0)))).((let H6 +\def (eq_ind A (ASort h1 n1) (\lambda (e: A).(match e in A return (\lambda +(_: A).Prop) with [(ASort _ _) \Rightarrow True | (AHead _ _) \Rightarrow +False])) I (AHead a (asucc g a0)) H4) in (False_ind ((eq A (ASort h2 n2) +(ASort O (next g n0))) \to ((eq A (aplus g (ASort h1 n1) k) (aplus g (ASort +h2 n2) k)) \to (leq g (AHead a a0) (ASort O n0)))) H6)) H5 H3))) | (leq_head +a3 a4 H3 a5 a6 H4) \Rightarrow (\lambda (H5: (eq A (AHead a3 a5) (AHead a +(asucc g a0)))).(\lambda (H6: (eq A (AHead a4 a6) (ASort O (next g +n0)))).((let H7 \def (f_equal A A (\lambda (e: A).(match e in A return +(\lambda (_: A).A) with [(ASort _ _) \Rightarrow a5 | (AHead _ a7) +\Rightarrow a7])) (AHead a3 a5) (AHead a (asucc g a0)) H5) in ((let H8 \def +(f_equal A A (\lambda (e: A).(match e in A return (\lambda (_: A).A) with +[(ASort _ _) \Rightarrow a3 | (AHead a7 _) \Rightarrow a7])) (AHead a3 a5) +(AHead a (asucc g a0)) H5) in (eq_ind A a (\lambda (a7: A).((eq A a5 (asucc g +a0)) \to ((eq A (AHead a4 a6) (ASort O (next g n0))) \to ((leq g a7 a4) \to +((leq g a5 a6) \to (leq g (AHead a a0) (ASort O n0))))))) (\lambda (H9: (eq A +a5 (asucc g a0))).(eq_ind A (asucc g a0) (\lambda (a7: A).((eq A (AHead a4 +a6) (ASort O (next g n0))) \to ((leq g a a4) \to ((leq g a7 a6) \to (leq g +(AHead a a0) (ASort O n0)))))) (\lambda (H10: (eq A (AHead a4 a6) (ASort O +(next g n0)))).(let H11 \def (eq_ind A (AHead a4 a6) (\lambda (e: A).(match e +in A return (\lambda (_: A).Prop) with [(ASort _ _) \Rightarrow False | +(AHead _ _) \Rightarrow True])) I (ASort O (next g n0)) H10) in (False_ind +((leq g a a4) \to ((leq g (asucc g a0) a6) \to (leq g (AHead a a0) (ASort O +n0)))) H11))) a5 (sym_eq A a5 (asucc g a0) H9))) a3 (sym_eq A a3 a H8))) H7)) +H6 H3 H4)))]) in (H3 (refl_equal A (AHead a (asucc g a0))) (refl_equal A +(ASort O (next g n0)))))) | (S n1) \Rightarrow (\lambda (H2: (leq g (asucc g +(AHead a a0)) (asucc g (ASort (S n1) n0)))).(let H3 \def (match H2 in leq +return (\lambda (a3: A).(\lambda (a4: A).(\lambda (_: (leq ? a3 a4)).((eq A +a3 (AHead a (asucc g a0))) \to ((eq A a4 (ASort n1 n0)) \to (leq g (AHead a +a0) (ASort (S n1) n0))))))) with [(leq_sort h1 h2 n2 n3 k H3) \Rightarrow +(\lambda (H4: (eq A (ASort h1 n2) (AHead a (asucc g a0)))).(\lambda (H5: (eq +A (ASort h2 n3) (ASort n1 n0))).((let H6 \def (eq_ind A (ASort h1 n2) +(\lambda (e: A).(match e in A return (\lambda (_: A).Prop) with [(ASort _ _) +\Rightarrow True | (AHead _ _) \Rightarrow False])) I (AHead a (asucc g a0)) +H4) in (False_ind ((eq A (ASort h2 n3) (ASort n1 n0)) \to ((eq A (aplus g +(ASort h1 n2) k) (aplus g (ASort h2 n3) k)) \to (leq g (AHead a a0) (ASort (S +n1) n0)))) H6)) H5 H3))) | (leq_head a3 a4 H3 a5 a6 H4) \Rightarrow (\lambda +(H5: (eq A (AHead a3 a5) (AHead a (asucc g a0)))).(\lambda (H6: (eq A (AHead +a4 a6) (ASort n1 n0))).((let H7 \def (f_equal A A (\lambda (e: A).(match e in +A return (\lambda (_: A).A) with [(ASort _ _) \Rightarrow a5 | (AHead _ a7) +\Rightarrow a7])) (AHead a3 a5) (AHead a (asucc g a0)) H5) in ((let H8 \def +(f_equal A A (\lambda (e: A).(match e in A return (\lambda (_: A).A) with +[(ASort _ _) \Rightarrow a3 | (AHead a7 _) \Rightarrow a7])) (AHead a3 a5) +(AHead a (asucc g a0)) H5) in (eq_ind A a (\lambda (a7: A).((eq A a5 (asucc g +a0)) \to ((eq A (AHead a4 a6) (ASort n1 n0)) \to ((leq g a7 a4) \to ((leq g +a5 a6) \to (leq g (AHead a a0) (ASort (S n1) n0))))))) (\lambda (H9: (eq A a5 +(asucc g a0))).(eq_ind A (asucc g a0) (\lambda (a7: A).((eq A (AHead a4 a6) +(ASort n1 n0)) \to ((leq g a a4) \to ((leq g a7 a6) \to (leq g (AHead a a0) +(ASort (S n1) n0)))))) (\lambda (H10: (eq A (AHead a4 a6) (ASort n1 +n0))).(let H11 \def (eq_ind A (AHead a4 a6) (\lambda (e: A).(match e in A +return (\lambda (_: A).Prop) with [(ASort _ _) \Rightarrow False | (AHead _ +_) \Rightarrow True])) I (ASort n1 n0) H10) in (False_ind ((leq g a a4) \to +((leq g (asucc g a0) a6) \to (leq g (AHead a a0) (ASort (S n1) n0)))) H11))) +a5 (sym_eq A a5 (asucc g a0) H9))) a3 (sym_eq A a3 a H8))) H7)) H6 H3 H4)))]) +in (H3 (refl_equal A (AHead a (asucc g a0))) (refl_equal A (ASort n1 +n0)))))]) H1)))) (\lambda (a3: A).(\lambda (_: (((leq g (asucc g (AHead a +a0)) (asucc g a3)) \to (leq g (AHead a a0) a3)))).(\lambda (a4: A).(\lambda +(_: (((leq g (asucc g (AHead a a0)) (asucc g a4)) \to (leq g (AHead a a0) +a4)))).(\lambda (H3: (leq g (asucc g (AHead a a0)) (asucc g (AHead a3 +a4)))).(let H4 \def (match H3 in leq return (\lambda (a5: A).(\lambda (a6: +A).(\lambda (_: (leq ? a5 a6)).((eq A a5 (AHead a (asucc g a0))) \to ((eq A +a6 (AHead a3 (asucc g a4))) \to (leq g (AHead a a0) (AHead a3 a4))))))) with +[(leq_sort h1 h2 n1 n2 k H4) \Rightarrow (\lambda (H5: (eq A (ASort h1 n1) +(AHead a (asucc g a0)))).(\lambda (H6: (eq A (ASort h2 n2) (AHead a3 (asucc g +a4)))).((let H7 \def (eq_ind A (ASort h1 n1) (\lambda (e: A).(match e in A +return (\lambda (_: A).Prop) with [(ASort _ _) \Rightarrow True | (AHead _ _) +\Rightarrow False])) I (AHead a (asucc g a0)) H5) in (False_ind ((eq A (ASort +h2 n2) (AHead a3 (asucc g a4))) \to ((eq A (aplus g (ASort h1 n1) k) (aplus g +(ASort h2 n2) k)) \to (leq g (AHead a a0) (AHead a3 a4)))) H7)) H6 H4))) | +(leq_head a5 a6 H4 a7 a8 H5) \Rightarrow (\lambda (H6: (eq A (AHead a5 a7) +(AHead a (asucc g a0)))).(\lambda (H7: (eq A (AHead a6 a8) (AHead a3 (asucc g +a4)))).((let H8 \def (f_equal A A (\lambda (e: A).(match e in A return +(\lambda (_: A).A) with [(ASort _ _) \Rightarrow a7 | (AHead _ a9) +\Rightarrow a9])) (AHead a5 a7) (AHead a (asucc g a0)) H6) in ((let H9 \def +(f_equal A A (\lambda (e: A).(match e in A return (\lambda (_: A).A) with +[(ASort _ _) \Rightarrow a5 | (AHead a9 _) \Rightarrow a9])) (AHead a5 a7) +(AHead a (asucc g a0)) H6) in (eq_ind A a (\lambda (a9: A).((eq A a7 (asucc g +a0)) \to ((eq A (AHead a6 a8) (AHead a3 (asucc g a4))) \to ((leq g a9 a6) \to +((leq g a7 a8) \to (leq g (AHead a a0) (AHead a3 a4))))))) (\lambda (H10: (eq +A a7 (asucc g a0))).(eq_ind A (asucc g a0) (\lambda (a9: A).((eq A (AHead a6 +a8) (AHead a3 (asucc g a4))) \to ((leq g a a6) \to ((leq g a9 a8) \to (leq g +(AHead a a0) (AHead a3 a4)))))) (\lambda (H11: (eq A (AHead a6 a8) (AHead a3 +(asucc g a4)))).(let H12 \def (f_equal A A (\lambda (e: A).(match e in A +return (\lambda (_: A).A) with [(ASort _ _) \Rightarrow a8 | (AHead _ a9) +\Rightarrow a9])) (AHead a6 a8) (AHead a3 (asucc g a4)) H11) in ((let H13 +\def (f_equal A A (\lambda (e: A).(match e in A return (\lambda (_: A).A) +with [(ASort _ _) \Rightarrow a6 | (AHead a9 _) \Rightarrow a9])) (AHead a6 +a8) (AHead a3 (asucc g a4)) H11) in (eq_ind A a3 (\lambda (a9: A).((eq A a8 +(asucc g a4)) \to ((leq g a a9) \to ((leq g (asucc g a0) a8) \to (leq g +(AHead a a0) (AHead a3 a4)))))) (\lambda (H14: (eq A a8 (asucc g +a4))).(eq_ind A (asucc g a4) (\lambda (a9: A).((leq g a a3) \to ((leq g +(asucc g a0) a9) \to (leq g (AHead a a0) (AHead a3 a4))))) (\lambda (H15: +(leq g a a3)).(\lambda (H16: (leq g (asucc g a0) (asucc g a4))).(leq_head g a +a3 H15 a0 a4 (H0 a4 H16)))) a8 (sym_eq A a8 (asucc g a4) H14))) a6 (sym_eq A +a6 a3 H13))) H12))) a7 (sym_eq A a7 (asucc g a0) H10))) a5 (sym_eq A a5 a +H9))) H8)) H7 H4 H5)))]) in (H4 (refl_equal A (AHead a (asucc g a0))) +(refl_equal A (AHead a3 (asucc g a4)))))))))) a2)))))) a1)). + +theorem leq_asucc: + \forall (g: G).(\forall (a: A).(ex A (\lambda (a0: A).(leq g a (asucc g +a0))))) +\def + \lambda (g: G).(\lambda (a: A).(A_ind (\lambda (a0: A).(ex A (\lambda (a1: +A).(leq g a0 (asucc g a1))))) (\lambda (n: nat).(\lambda (n0: nat).(ex_intro +A (\lambda (a0: A).(leq g (ASort n n0) (asucc g a0))) (ASort (S n) n0) +(leq_refl g (ASort n n0))))) (\lambda (a0: A).(\lambda (_: (ex A (\lambda +(a1: A).(leq g a0 (asucc g a1))))).(\lambda (a1: A).(\lambda (H0: (ex A +(\lambda (a2: A).(leq g a1 (asucc g a2))))).(let H1 \def H0 in (ex_ind A +(\lambda (a2: A).(leq g a1 (asucc g a2))) (ex A (\lambda (a2: A).(leq g +(AHead a0 a1) (asucc g a2)))) (\lambda (x: A).(\lambda (H2: (leq g a1 (asucc +g x))).(ex_intro A (\lambda (a2: A).(leq g (AHead a0 a1) (asucc g a2))) +(AHead a0 x) (leq_head g a0 a0 (leq_refl g a0) a1 (asucc g x) H2)))) H1)))))) +a)). + +theorem leq_ahead_asucc_false: + \forall (g: G).(\forall (a1: A).(\forall (a2: A).((leq g (AHead a1 a2) +(asucc g a1)) \to (\forall (P: Prop).P)))) +\def + \lambda (g: G).(\lambda (a1: A).(A_ind (\lambda (a: A).(\forall (a2: +A).((leq g (AHead a a2) (asucc g a)) \to (\forall (P: Prop).P)))) (\lambda +(n: nat).(\lambda (n0: nat).(\lambda (a2: A).(\lambda (H: (leq g (AHead +(ASort n n0) a2) (match n with [O \Rightarrow (ASort O (next g n0)) | (S h) +\Rightarrow (ASort h n0)]))).(\lambda (P: Prop).((match n in nat return +(\lambda (n1: nat).((leq g (AHead (ASort n1 n0) a2) (match n1 with [O +\Rightarrow (ASort O (next g n0)) | (S h) \Rightarrow (ASort h n0)])) \to P)) +with [O \Rightarrow (\lambda (H0: (leq g (AHead (ASort O n0) a2) (ASort O +(next g n0)))).(let H1 \def (match H0 in leq return (\lambda (a: A).(\lambda +(a0: A).(\lambda (_: (leq ? a a0)).((eq A a (AHead (ASort O n0) a2)) \to ((eq +A a0 (ASort O (next g n0))) \to P))))) with [(leq_sort h1 h2 n1 n2 k H1) +\Rightarrow (\lambda (H2: (eq A (ASort h1 n1) (AHead (ASort O n0) +a2))).(\lambda (H3: (eq A (ASort h2 n2) (ASort O (next g n0)))).((let H4 \def +(eq_ind A (ASort h1 n1) (\lambda (e: A).(match e in A return (\lambda (_: +A).Prop) with [(ASort _ _) \Rightarrow True | (AHead _ _) \Rightarrow +False])) I (AHead (ASort O n0) a2) H2) in (False_ind ((eq A (ASort h2 n2) +(ASort O (next g n0))) \to ((eq A (aplus g (ASort h1 n1) k) (aplus g (ASort +h2 n2) k)) \to P)) H4)) H3 H1))) | (leq_head a0 a3 H1 a4 a5 H2) \Rightarrow +(\lambda (H3: (eq A (AHead a0 a4) (AHead (ASort O n0) a2))).(\lambda (H4: (eq +A (AHead a3 a5) (ASort O (next g n0)))).((let H5 \def (f_equal A A (\lambda +(e: A).(match e in A return (\lambda (_: A).A) with [(ASort _ _) \Rightarrow +a4 | (AHead _ a) \Rightarrow a])) (AHead a0 a4) (AHead (ASort O n0) a2) H3) +in ((let H6 \def (f_equal A A (\lambda (e: A).(match e in A return (\lambda +(_: A).A) with [(ASort _ _) \Rightarrow a0 | (AHead a _) \Rightarrow a])) +(AHead a0 a4) (AHead (ASort O n0) a2) H3) in (eq_ind A (ASort O n0) (\lambda +(a: A).((eq A a4 a2) \to ((eq A (AHead a3 a5) (ASort O (next g n0))) \to +((leq g a a3) \to ((leq g a4 a5) \to P))))) (\lambda (H7: (eq A a4 +a2)).(eq_ind A a2 (\lambda (a: A).((eq A (AHead a3 a5) (ASort O (next g n0))) +\to ((leq g (ASort O n0) a3) \to ((leq g a a5) \to P)))) (\lambda (H8: (eq A +(AHead a3 a5) (ASort O (next g n0)))).(let H9 \def (eq_ind A (AHead a3 a5) +(\lambda (e: A).(match e in A return (\lambda (_: A).Prop) with [(ASort _ _) +\Rightarrow False | (AHead _ _) \Rightarrow True])) I (ASort O (next g n0)) +H8) in (False_ind ((leq g (ASort O n0) a3) \to ((leq g a2 a5) \to P)) H9))) +a4 (sym_eq A a4 a2 H7))) a0 (sym_eq A a0 (ASort O n0) H6))) H5)) H4 H1 +H2)))]) in (H1 (refl_equal A (AHead (ASort O n0) a2)) (refl_equal A (ASort O +(next g n0)))))) | (S n1) \Rightarrow (\lambda (H0: (leq g (AHead (ASort (S +n1) n0) a2) (ASort n1 n0))).(let H1 \def (match H0 in leq return (\lambda (a: +A).(\lambda (a0: A).(\lambda (_: (leq ? a a0)).((eq A a (AHead (ASort (S n1) +n0) a2)) \to ((eq A a0 (ASort n1 n0)) \to P))))) with [(leq_sort h1 h2 n2 n3 +k H1) \Rightarrow (\lambda (H2: (eq A (ASort h1 n2) (AHead (ASort (S n1) n0) +a2))).(\lambda (H3: (eq A (ASort h2 n3) (ASort n1 n0))).((let H4 \def (eq_ind +A (ASort h1 n2) (\lambda (e: A).(match e in A return (\lambda (_: A).Prop) +with [(ASort _ _) \Rightarrow True | (AHead _ _) \Rightarrow False])) I +(AHead (ASort (S n1) n0) a2) H2) in (False_ind ((eq A (ASort h2 n3) (ASort n1 +n0)) \to ((eq A (aplus g (ASort h1 n2) k) (aplus g (ASort h2 n3) k)) \to P)) +H4)) H3 H1))) | (leq_head a0 a3 H1 a4 a5 H2) \Rightarrow (\lambda (H3: (eq A +(AHead a0 a4) (AHead (ASort (S n1) n0) a2))).(\lambda (H4: (eq A (AHead a3 +a5) (ASort n1 n0))).((let H5 \def (f_equal A A (\lambda (e: A).(match e in A +return (\lambda (_: A).A) with [(ASort _ _) \Rightarrow a4 | (AHead _ a) +\Rightarrow a])) (AHead a0 a4) (AHead (ASort (S n1) n0) a2) H3) in ((let H6 +\def (f_equal A A (\lambda (e: A).(match e in A return (\lambda (_: A).A) +with [(ASort _ _) \Rightarrow a0 | (AHead a _) \Rightarrow a])) (AHead a0 a4) +(AHead (ASort (S n1) n0) a2) H3) in (eq_ind A (ASort (S n1) n0) (\lambda (a: +A).((eq A a4 a2) \to ((eq A (AHead a3 a5) (ASort n1 n0)) \to ((leq g a a3) +\to ((leq g a4 a5) \to P))))) (\lambda (H7: (eq A a4 a2)).(eq_ind A a2 +(\lambda (a: A).((eq A (AHead a3 a5) (ASort n1 n0)) \to ((leq g (ASort (S n1) +n0) a3) \to ((leq g a a5) \to P)))) (\lambda (H8: (eq A (AHead a3 a5) (ASort +n1 n0))).(let H9 \def (eq_ind A (AHead a3 a5) (\lambda (e: A).(match e in A +return (\lambda (_: A).Prop) with [(ASort _ _) \Rightarrow False | (AHead _ +_) \Rightarrow True])) I (ASort n1 n0) H8) in (False_ind ((leq g (ASort (S +n1) n0) a3) \to ((leq g a2 a5) \to P)) H9))) a4 (sym_eq A a4 a2 H7))) a0 +(sym_eq A a0 (ASort (S n1) n0) H6))) H5)) H4 H1 H2)))]) in (H1 (refl_equal A +(AHead (ASort (S n1) n0) a2)) (refl_equal A (ASort n1 n0)))))]) H)))))) +(\lambda (a: A).(\lambda (_: ((\forall (a2: A).((leq g (AHead a a2) (asucc g +a)) \to (\forall (P: Prop).P))))).(\lambda (a0: A).(\lambda (_: ((\forall +(a2: A).((leq g (AHead a0 a2) (asucc g a0)) \to (\forall (P: +Prop).P))))).(\lambda (a2: A).(\lambda (H1: (leq g (AHead (AHead a a0) a2) +(AHead a (asucc g a0)))).(\lambda (P: Prop).(let H2 \def (match H1 in leq +return (\lambda (a3: A).(\lambda (a4: A).(\lambda (_: (leq ? a3 a4)).((eq A +a3 (AHead (AHead a a0) a2)) \to ((eq A a4 (AHead a (asucc g a0))) \to P))))) +with [(leq_sort h1 h2 n1 n2 k H2) \Rightarrow (\lambda (H3: (eq A (ASort h1 +n1) (AHead (AHead a a0) a2))).(\lambda (H4: (eq A (ASort h2 n2) (AHead a +(asucc g a0)))).((let H5 \def (eq_ind A (ASort h1 n1) (\lambda (e: A).(match +e in A return (\lambda (_: A).Prop) with [(ASort _ _) \Rightarrow True | +(AHead _ _) \Rightarrow False])) I (AHead (AHead a a0) a2) H3) in (False_ind +((eq A (ASort h2 n2) (AHead a (asucc g a0))) \to ((eq A (aplus g (ASort h1 +n1) k) (aplus g (ASort h2 n2) k)) \to P)) H5)) H4 H2))) | (leq_head a3 a4 H2 +a5 a6 H3) \Rightarrow (\lambda (H4: (eq A (AHead a3 a5) (AHead (AHead a a0) +a2))).(\lambda (H5: (eq A (AHead a4 a6) (AHead a (asucc g a0)))).((let H6 +\def (f_equal A A (\lambda (e: A).(match e in A return (\lambda (_: A).A) +with [(ASort _ _) \Rightarrow a5 | (AHead _ a7) \Rightarrow a7])) (AHead a3 +a5) (AHead (AHead a a0) a2) H4) in ((let H7 \def (f_equal A A (\lambda (e: +A).(match e in A return (\lambda (_: A).A) with [(ASort _ _) \Rightarrow a3 | +(AHead a7 _) \Rightarrow a7])) (AHead a3 a5) (AHead (AHead a a0) a2) H4) in +(eq_ind A (AHead a a0) (\lambda (a7: A).((eq A a5 a2) \to ((eq A (AHead a4 +a6) (AHead a (asucc g a0))) \to ((leq g a7 a4) \to ((leq g a5 a6) \to P))))) +(\lambda (H8: (eq A a5 a2)).(eq_ind A a2 (\lambda (a7: A).((eq A (AHead a4 +a6) (AHead a (asucc g a0))) \to ((leq g (AHead a a0) a4) \to ((leq g a7 a6) +\to P)))) (\lambda (H9: (eq A (AHead a4 a6) (AHead a (asucc g a0)))).(let H10 +\def (f_equal A A (\lambda (e: A).(match e in A return (\lambda (_: A).A) +with [(ASort _ _) \Rightarrow a6 | (AHead _ a7) \Rightarrow a7])) (AHead a4 +a6) (AHead a (asucc g a0)) H9) in ((let H11 \def (f_equal A A (\lambda (e: +A).(match e in A return (\lambda (_: A).A) with [(ASort _ _) \Rightarrow a4 | +(AHead a7 _) \Rightarrow a7])) (AHead a4 a6) (AHead a (asucc g a0)) H9) in +(eq_ind A a (\lambda (a7: A).((eq A a6 (asucc g a0)) \to ((leq g (AHead a a0) +a7) \to ((leq g a2 a6) \to P)))) (\lambda (H12: (eq A a6 (asucc g +a0))).(eq_ind A (asucc g a0) (\lambda (a7: A).((leq g (AHead a a0) a) \to +((leq g a2 a7) \to P))) (\lambda (H13: (leq g (AHead a a0) a)).(\lambda (_: +(leq g a2 (asucc g a0))).(leq_ahead_false g a a0 H13 P))) a6 (sym_eq A a6 +(asucc g a0) H12))) a4 (sym_eq A a4 a H11))) H10))) a5 (sym_eq A a5 a2 H8))) +a3 (sym_eq A a3 (AHead a a0) H7))) H6)) H5 H2 H3)))]) in (H2 (refl_equal A +(AHead (AHead a a0) a2)) (refl_equal A (AHead a (asucc g a0)))))))))))) a1)). + +theorem leq_asucc_false: + \forall (g: G).(\forall (a: A).((leq g (asucc g a) a) \to (\forall (P: +Prop).P))) +\def + \lambda (g: G).(\lambda (a: A).(A_ind (\lambda (a0: A).((leq g (asucc g a0) +a0) \to (\forall (P: Prop).P))) (\lambda (n: nat).(\lambda (n0: nat).(\lambda +(H: (leq g (match n with [O \Rightarrow (ASort O (next g n0)) | (S h) +\Rightarrow (ASort h n0)]) (ASort n n0))).(\lambda (P: Prop).((match n in nat +return (\lambda (n1: nat).((leq g (match n1 with [O \Rightarrow (ASort O +(next g n0)) | (S h) \Rightarrow (ASort h n0)]) (ASort n1 n0)) \to P)) with +[O \Rightarrow (\lambda (H0: (leq g (ASort O (next g n0)) (ASort O n0))).(let +H1 \def (match H0 in leq return (\lambda (a0: A).(\lambda (a1: A).(\lambda +(_: (leq ? a0 a1)).((eq A a0 (ASort O (next g n0))) \to ((eq A a1 (ASort O +n0)) \to P))))) with [(leq_sort h1 h2 n1 n2 k H1) \Rightarrow (\lambda (H2: +(eq A (ASort h1 n1) (ASort O (next g n0)))).(\lambda (H3: (eq A (ASort h2 n2) +(ASort O n0))).((let H4 \def (f_equal A nat (\lambda (e: A).(match e in A +return (\lambda (_: A).nat) with [(ASort _ n3) \Rightarrow n3 | (AHead _ _) +\Rightarrow n1])) (ASort h1 n1) (ASort O (next g n0)) H2) in ((let H5 \def +(f_equal A nat (\lambda (e: A).(match e in A return (\lambda (_: A).nat) with +[(ASort n3 _) \Rightarrow n3 | (AHead _ _) \Rightarrow h1])) (ASort h1 n1) +(ASort O (next g n0)) H2) in (eq_ind nat O (\lambda (n3: nat).((eq nat n1 +(next g n0)) \to ((eq A (ASort h2 n2) (ASort O n0)) \to ((eq A (aplus g +(ASort n3 n1) k) (aplus g (ASort h2 n2) k)) \to P)))) (\lambda (H6: (eq nat +n1 (next g n0))).(eq_ind nat (next g n0) (\lambda (n3: nat).((eq A (ASort h2 +n2) (ASort O n0)) \to ((eq A (aplus g (ASort O n3) k) (aplus g (ASort h2 n2) +k)) \to P))) (\lambda (H7: (eq A (ASort h2 n2) (ASort O n0))).(let H8 \def +(f_equal A nat (\lambda (e: A).(match e in A return (\lambda (_: A).nat) with +[(ASort _ n3) \Rightarrow n3 | (AHead _ _) \Rightarrow n2])) (ASort h2 n2) +(ASort O n0) H7) in ((let H9 \def (f_equal A nat (\lambda (e: A).(match e in +A return (\lambda (_: A).nat) with [(ASort n3 _) \Rightarrow n3 | (AHead _ _) +\Rightarrow h2])) (ASort h2 n2) (ASort O n0) H7) in (eq_ind nat O (\lambda +(n3: nat).((eq nat n2 n0) \to ((eq A (aplus g (ASort O (next g n0)) k) (aplus +g (ASort n3 n2) k)) \to P))) (\lambda (H10: (eq nat n2 n0)).(eq_ind nat n0 +(\lambda (n3: nat).((eq A (aplus g (ASort O (next g n0)) k) (aplus g (ASort O +n3) k)) \to P)) (\lambda (H11: (eq A (aplus g (ASort O (next g n0)) k) (aplus +g (ASort O n0) k))).(let H12 \def (eq_ind_r A (aplus g (ASort O (next g n0)) +k) (\lambda (a0: A).(eq A a0 (aplus g (ASort O n0) k))) H11 (aplus g (ASort O +n0) (S k)) (aplus_sort_O_S_simpl g n0 k)) in (let H_y \def (aplus_inj g (S k) +k (ASort O n0) H12) in (le_Sx_x k (eq_ind_r nat k (\lambda (n3: nat).(le n3 +k)) (le_n k) (S k) H_y) P)))) n2 (sym_eq nat n2 n0 H10))) h2 (sym_eq nat h2 O +H9))) H8))) n1 (sym_eq nat n1 (next g n0) H6))) h1 (sym_eq nat h1 O H5))) +H4)) H3 H1))) | (leq_head a1 a2 H1 a3 a4 H2) \Rightarrow (\lambda (H3: (eq A +(AHead a1 a3) (ASort O (next g n0)))).(\lambda (H4: (eq A (AHead a2 a4) +(ASort O n0))).((let H5 \def (eq_ind A (AHead a1 a3) (\lambda (e: A).(match e +in A return (\lambda (_: A).Prop) with [(ASort _ _) \Rightarrow False | +(AHead _ _) \Rightarrow True])) I (ASort O (next g n0)) H3) in (False_ind +((eq A (AHead a2 a4) (ASort O n0)) \to ((leq g a1 a2) \to ((leq g a3 a4) \to +P))) H5)) H4 H1 H2)))]) in (H1 (refl_equal A (ASort O (next g n0))) +(refl_equal A (ASort O n0))))) | (S n1) \Rightarrow (\lambda (H0: (leq g +(ASort n1 n0) (ASort (S n1) n0))).(let H1 \def (match H0 in leq return +(\lambda (a0: A).(\lambda (a1: A).(\lambda (_: (leq ? a0 a1)).((eq A a0 +(ASort n1 n0)) \to ((eq A a1 (ASort (S n1) n0)) \to P))))) with [(leq_sort h1 +h2 n2 n3 k H1) \Rightarrow (\lambda (H2: (eq A (ASort h1 n2) (ASort n1 +n0))).(\lambda (H3: (eq A (ASort h2 n3) (ASort (S n1) n0))).((let H4 \def +(f_equal A nat (\lambda (e: A).(match e in A return (\lambda (_: A).nat) with +[(ASort _ n4) \Rightarrow n4 | (AHead _ _) \Rightarrow n2])) (ASort h1 n2) +(ASort n1 n0) H2) in ((let H5 \def (f_equal A nat (\lambda (e: A).(match e in +A return (\lambda (_: A).nat) with [(ASort n4 _) \Rightarrow n4 | (AHead _ _) +\Rightarrow h1])) (ASort h1 n2) (ASort n1 n0) H2) in (eq_ind nat n1 (\lambda +(n4: nat).((eq nat n2 n0) \to ((eq A (ASort h2 n3) (ASort (S n1) n0)) \to +((eq A (aplus g (ASort n4 n2) k) (aplus g (ASort h2 n3) k)) \to P)))) +(\lambda (H6: (eq nat n2 n0)).(eq_ind nat n0 (\lambda (n4: nat).((eq A (ASort +h2 n3) (ASort (S n1) n0)) \to ((eq A (aplus g (ASort n1 n4) k) (aplus g +(ASort h2 n3) k)) \to P))) (\lambda (H7: (eq A (ASort h2 n3) (ASort (S n1) +n0))).(let H8 \def (f_equal A nat (\lambda (e: A).(match e in A return +(\lambda (_: A).nat) with [(ASort _ n4) \Rightarrow n4 | (AHead _ _) +\Rightarrow n3])) (ASort h2 n3) (ASort (S n1) n0) H7) in ((let H9 \def +(f_equal A nat (\lambda (e: A).(match e in A return (\lambda (_: A).nat) with +[(ASort n4 _) \Rightarrow n4 | (AHead _ _) \Rightarrow h2])) (ASort h2 n3) +(ASort (S n1) n0) H7) in (eq_ind nat (S n1) (\lambda (n4: nat).((eq nat n3 +n0) \to ((eq A (aplus g (ASort n1 n0) k) (aplus g (ASort n4 n3) k)) \to P))) +(\lambda (H10: (eq nat n3 n0)).(eq_ind nat n0 (\lambda (n4: nat).((eq A +(aplus g (ASort n1 n0) k) (aplus g (ASort (S n1) n4) k)) \to P)) (\lambda +(H11: (eq A (aplus g (ASort n1 n0) k) (aplus g (ASort (S n1) n0) k))).(let +H12 \def (eq_ind_r A (aplus g (ASort n1 n0) k) (\lambda (a0: A).(eq A a0 +(aplus g (ASort (S n1) n0) k))) H11 (aplus g (ASort (S n1) n0) (S k)) +(aplus_sort_S_S_simpl g n0 n1 k)) in (let H_y \def (aplus_inj g (S k) k +(ASort (S n1) n0) H12) in (le_Sx_x k (eq_ind_r nat k (\lambda (n4: nat).(le +n4 k)) (le_n k) (S k) H_y) P)))) n3 (sym_eq nat n3 n0 H10))) h2 (sym_eq nat +h2 (S n1) H9))) H8))) n2 (sym_eq nat n2 n0 H6))) h1 (sym_eq nat h1 n1 H5))) +H4)) H3 H1))) | (leq_head a1 a2 H1 a3 a4 H2) \Rightarrow (\lambda (H3: (eq A +(AHead a1 a3) (ASort n1 n0))).(\lambda (H4: (eq A (AHead a2 a4) (ASort (S n1) +n0))).((let H5 \def (eq_ind A (AHead a1 a3) (\lambda (e: A).(match e in A +return (\lambda (_: A).Prop) with [(ASort _ _) \Rightarrow False | (AHead _ +_) \Rightarrow True])) I (ASort n1 n0) H3) in (False_ind ((eq A (AHead a2 a4) +(ASort (S n1) n0)) \to ((leq g a1 a2) \to ((leq g a3 a4) \to P))) H5)) H4 H1 +H2)))]) in (H1 (refl_equal A (ASort n1 n0)) (refl_equal A (ASort (S n1) +n0)))))]) H))))) (\lambda (a0: A).(\lambda (_: (((leq g (asucc g a0) a0) \to +(\forall (P: Prop).P)))).(\lambda (a1: A).(\lambda (H0: (((leq g (asucc g a1) +a1) \to (\forall (P: Prop).P)))).(\lambda (H1: (leq g (AHead a0 (asucc g a1)) +(AHead a0 a1))).(\lambda (P: Prop).(let H2 \def (match H1 in leq return +(\lambda (a2: A).(\lambda (a3: A).(\lambda (_: (leq ? a2 a3)).((eq A a2 +(AHead a0 (asucc g a1))) \to ((eq A a3 (AHead a0 a1)) \to P))))) with +[(leq_sort h1 h2 n1 n2 k H2) \Rightarrow (\lambda (H3: (eq A (ASort h1 n1) +(AHead a0 (asucc g a1)))).(\lambda (H4: (eq A (ASort h2 n2) (AHead a0 +a1))).((let H5 \def (eq_ind A (ASort h1 n1) (\lambda (e: A).(match e in A +return (\lambda (_: A).Prop) with [(ASort _ _) \Rightarrow True | (AHead _ _) +\Rightarrow False])) I (AHead a0 (asucc g a1)) H3) in (False_ind ((eq A +(ASort h2 n2) (AHead a0 a1)) \to ((eq A (aplus g (ASort h1 n1) k) (aplus g +(ASort h2 n2) k)) \to P)) H5)) H4 H2))) | (leq_head a2 a3 H2 a4 a5 H3) +\Rightarrow (\lambda (H4: (eq A (AHead a2 a4) (AHead a0 (asucc g +a1)))).(\lambda (H5: (eq A (AHead a3 a5) (AHead a0 a1))).((let H6 \def +(f_equal A A (\lambda (e: A).(match e in A return (\lambda (_: A).A) with +[(ASort _ _) \Rightarrow a4 | (AHead _ a6) \Rightarrow a6])) (AHead a2 a4) +(AHead a0 (asucc g a1)) H4) in ((let H7 \def (f_equal A A (\lambda (e: +A).(match e in A return (\lambda (_: A).A) with [(ASort _ _) \Rightarrow a2 | +(AHead a6 _) \Rightarrow a6])) (AHead a2 a4) (AHead a0 (asucc g a1)) H4) in +(eq_ind A a0 (\lambda (a6: A).((eq A a4 (asucc g a1)) \to ((eq A (AHead a3 +a5) (AHead a0 a1)) \to ((leq g a6 a3) \to ((leq g a4 a5) \to P))))) (\lambda +(H8: (eq A a4 (asucc g a1))).(eq_ind A (asucc g a1) (\lambda (a6: A).((eq A +(AHead a3 a5) (AHead a0 a1)) \to ((leq g a0 a3) \to ((leq g a6 a5) \to P)))) +(\lambda (H9: (eq A (AHead a3 a5) (AHead a0 a1))).(let H10 \def (f_equal A A +(\lambda (e: A).(match e in A return (\lambda (_: A).A) with [(ASort _ _) +\Rightarrow a5 | (AHead _ a6) \Rightarrow a6])) (AHead a3 a5) (AHead a0 a1) +H9) in ((let H11 \def (f_equal A A (\lambda (e: A).(match e in A return +(\lambda (_: A).A) with [(ASort _ _) \Rightarrow a3 | (AHead a6 _) +\Rightarrow a6])) (AHead a3 a5) (AHead a0 a1) H9) in (eq_ind A a0 (\lambda +(a6: A).((eq A a5 a1) \to ((leq g a0 a6) \to ((leq g (asucc g a1) a5) \to +P)))) (\lambda (H12: (eq A a5 a1)).(eq_ind A a1 (\lambda (a6: A).((leq g a0 +a0) \to ((leq g (asucc g a1) a6) \to P))) (\lambda (_: (leq g a0 +a0)).(\lambda (H14: (leq g (asucc g a1) a1)).(H0 H14 P))) a5 (sym_eq A a5 a1 +H12))) a3 (sym_eq A a3 a0 H11))) H10))) a4 (sym_eq A a4 (asucc g a1) H8))) a2 +(sym_eq A a2 a0 H7))) H6)) H5 H2 H3)))]) in (H2 (refl_equal A (AHead a0 +(asucc g a1))) (refl_equal A (AHead a0 a1)))))))))) a)). diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/theory.ma b/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/theory.ma index 405f95aff..8b96936ab 100644 --- a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/theory.ma +++ b/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/theory.ma @@ -176,5 +176,7 @@ include "aplus/props.ma". include "leq/defs.ma". +include "leq/props.ma". + include "leq/asucc.ma". diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/problems-1.ma b/matita/contribs/LAMBDA-TYPES/Level-1/problems-1.ma deleted file mode 100644 index 0c747cdf0..000000000 --- a/matita/contribs/LAMBDA-TYPES/Level-1/problems-1.ma +++ /dev/null @@ -1,106 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -(* Problematic objects for disambiguation/typechecking ********************) - -set "baseuri" "cic:/matita/LAMBDA-TYPES/Level-1/problems". - -include "LambdaDelta/theory.ma". - -theorem iso_trans: - \forall (t1: T).(\forall (t2: T).((iso t1 t2) \to (\forall (t3: T).((iso t2 -t3) \to (iso t1 t3))))) -\def - \lambda (t1: T).(\lambda (t2: T).(\lambda (H: (iso t1 t2)).(iso_ind (\lambda -(t: T).(\lambda (t0: T).(\forall (t3: T).((iso t0 t3) \to (iso t t3))))) -(\lambda (n1: nat).(\lambda (n2: nat).(\lambda (t3: T).(\lambda (H0: (iso -(TSort n2) t3)).(let H1 \def (match H0 in iso return (\lambda (t: T).(\lambda -(t0: T).(\lambda (_: (iso t t0)).((eq T t (TSort n2)) \to ((eq T t0 t3) \to -(iso (TSort n1) t3)))))) with [(iso_sort n0 n3) \Rightarrow (\lambda (H0: (eq -T (TSort n0) (TSort n2))).(\lambda (H1: (eq T (TSort n3) t3)).((let H2 \def -(f_equal T nat (\lambda (e: T).(match e in T return (\lambda (_: T).nat) with -[(TSort n) \Rightarrow n | (TLRef _) \Rightarrow n0 | (THead _ _ _) -\Rightarrow n0])) (TSort n0) (TSort n2) H0) in (eq_ind nat n2 (\lambda (_: -nat).((eq T (TSort n3) t3) \to (iso (TSort n1) t3))) (\lambda (H3: (eq T -(TSort n3) t3)).(eq_ind T (TSort n3) (\lambda (t: T).(iso (TSort n1) t)) -(iso_sort n1 n3) t3 H3)) n0 (sym_eq nat n0 n2 H2))) H1))) | (iso_lref i1 i2) -\Rightarrow (\lambda (H0: (eq T (TLRef i1) (TSort n2))).(\lambda (H1: (eq T -(TLRef i2) t3)).((let H2 \def (eq_ind T (TLRef i1) (\lambda (e: T).(match e -in T return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef -_) \Rightarrow True | (THead _ _ _) \Rightarrow False])) I (TSort n2) H0) in -(False_ind ((eq T (TLRef i2) t3) \to (iso (TSort n1) t3)) H2)) H1))) | -(iso_head k v1 v2 t1 t2) \Rightarrow (\lambda (H0: (eq T (THead k v1 t1) -(TSort n2))).(\lambda (H1: (eq T (THead k v2 t2) t3)).((let H2 \def (eq_ind T -(THead k v1 t1) (\lambda (e: T).(match e in T return (\lambda (_: T).Prop) -with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow False | (THead _ _ -_) \Rightarrow True])) I (TSort n2) H0) in (False_ind ((eq T (THead k v2 t2) -t3) \to (iso (TSort n1) t3)) H2)) H1)))]) in (H1 (refl_equal T (TSort n2)) -(refl_equal T t3))))))) (\lambda (i1: nat).(\lambda (i2: nat).(\lambda (t3: -T).(\lambda (H0: (iso (TLRef i2) t3)).(let H1 \def (match H0 in iso return -(\lambda (t: T).(\lambda (t0: T).(\lambda (_: (iso t t0)).((eq T t (TLRef -i2)) \to ((eq T t0 t3) \to (iso (TLRef i1) t3)))))) with [(iso_sort n1 n2) -\Rightarrow (\lambda (H0: (eq T (TSort n1) (TLRef i2))).(\lambda (H1: (eq T -(TSort n2) t3)).((let H2 \def (eq_ind T (TSort n1) (\lambda (e: T).(match e -in T return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow True | (TLRef -_) \Rightarrow False | (THead _ _ _) \Rightarrow False])) I (TLRef i2) H0) in -(False_ind ((eq T (TSort n2) t3) \to (iso (TLRef i1) t3)) H2)) H1))) | -(iso_lref i0 i3) \Rightarrow (\lambda (H0: (eq T (TLRef i0) (TLRef -i2))).(\lambda (H1: (eq T (TLRef i3) t3)).((let H2 \def (f_equal T nat -(\lambda (e: T).(match e in T return (\lambda (_: T).nat) with [(TSort _) -\Rightarrow i0 | (TLRef n) \Rightarrow n | (THead _ _ _) \Rightarrow i0])) -(TLRef i0) (TLRef i2) H0) in (eq_ind nat i2 (\lambda (_: nat).((eq T (TLRef -i3) t3) \to (iso (TLRef i1) t3))) (\lambda (H3: (eq T (TLRef i3) t3)).(eq_ind -T (TLRef i3) (\lambda (t: T).(iso (TLRef i1) t)) (iso_lref i1 i3) t3 H3)) i0 -(sym_eq nat i0 i2 H2))) H1))) | (iso_head k v1 v2 t1 t2) \Rightarrow (\lambda -(H0: (eq T (THead k v1 t1) (TLRef i2))).(\lambda (H1: (eq T (THead k v2 t2) -t3)).((let H2 \def (eq_ind T (THead k v1 t1) (\lambda (e: T).(match e in T -return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef _) -\Rightarrow False | (THead _ _ _) \Rightarrow True])) I (TLRef i2) H0) in -(False_ind ((eq T (THead k v2 t2) t3) \to (iso (TLRef i1) t3)) H2)) H1)))]) -in (H1 (refl_equal T (TLRef i2)) (refl_equal T t3))))))) (\lambda (k: -K).(\lambda (v1: T).(\lambda (v2: T).(\lambda (t3: T).(\lambda (t4: -T).(\lambda (t5: T).(\lambda (H0: (iso (THead k v2 t4) t5)).(let H1 \def -(match H0 in iso return (\lambda (t: T).(\lambda (t0: T).(\lambda (_: (iso t -t0)).((eq T t (THead k v2 t4)) \to ((eq T t0 t5) \to (iso (THead k v1 t3) -t5)))))) with [(iso_sort n1 n2) \Rightarrow (\lambda (H0: (eq T (TSort n1) -(THead k v2 t4))).(\lambda (H1: (eq T (TSort n2) t5)).((let H2 \def (eq_ind T -(TSort n1) (\lambda (e: T).(match e in T return (\lambda (_: T).Prop) with -[(TSort _) \Rightarrow True | (TLRef _) \Rightarrow False | (THead _ _ _) -\Rightarrow False])) I (THead k v2 t4) H0) in (False_ind ((eq T (TSort n2) -t5) \to (iso (THead k v1 t3) t5)) H2)) H1))) | (iso_lref i1 i2) \Rightarrow -(\lambda (H0: (eq T (TLRef i1) (THead k v2 t4))).(\lambda (H1: (eq T (TLRef -i2) t5)).((let H2 \def (eq_ind T (TLRef i1) (\lambda (e: T).(match e in T -return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef _) -\Rightarrow True | (THead _ _ _) \Rightarrow False])) I (THead k v2 t4) H0) -in (False_ind ((eq T (TLRef i2) t5) \to (iso (THead k v1 t3) t5)) H2)) H1))) -| (iso_head k0 v0 v3 t0 t4) \Rightarrow (\lambda (H0: (eq T (THead k0 v0 t0) -(THead k v2 t4))).(\lambda (H1: (eq T (THead k0 v3 t4) t5)).((let H2 \def -(f_equal T T (\lambda (e: T).(match e in T return (\lambda (_: T).T) with -[(TSort _) \Rightarrow t0 | (TLRef _) \Rightarrow t0 | (THead _ _ t) -\Rightarrow t])) (THead k0 v0 t0) (THead k v2 t4) H0) in ((let H3 \def -(f_equal T T (\lambda (e: T).(match e in T return (\lambda (_: T).T) with -[(TSort _) \Rightarrow v0 | (TLRef _) \Rightarrow v0 | (THead _ t _) -\Rightarrow t])) (THead k0 v0 t0) (THead k v2 t4) H0) in ((let H4 \def -(f_equal T K (\lambda (e: T).(match e in T return (\lambda (_: T).K) with -[(TSort _) \Rightarrow k0 | (TLRef _) \Rightarrow k0 | (THead k _ _) -\Rightarrow k])) (THead k0 v0 t0) (THead k v2 t4) H0) in (eq_ind K k (\lambda -(k1: K).((eq T v0 v2) \to ((eq T t0 t4) \to ((eq T (THead k1 v3 t4) t5) \to -(iso (THead k v1 t3) t5))))) (\lambda (H5: (eq T v0 v2)).(eq_ind T v2 -(\lambda (_: T).((eq T t0 t4) \to ((eq T (THead k v3 t4) t5) \to (iso (THead -k v1 t3) t5)))) (\lambda (H6: (eq T t0 t4)).(eq_ind T t4 (\lambda (_: T).((eq -T (THead k v3 t4) t5) \to (iso (THead k v1 t3) t5))) (\lambda (H7: (eq T -(THead k v3 t4) t5)).(eq_ind T (THead k v3 t4) (\lambda (t: T).(iso (THead k -v1 t3) t)) (iso_head k v1 v3 t3 t4) t5 H7)) t0 (sym_eq T t0 t4 H6))) v0 -(sym_eq T v0 v2 H5))) k0 (sym_eq K k0 k H4))) H3)) H2)) H1)))]) in (H1 -(refl_equal T (THead k v2 t4)) (refl_equal T t5)))))))))) t1 t2 H))). diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/problems-2.ma b/matita/contribs/LAMBDA-TYPES/Level-1/problems-2.ma deleted file mode 100644 index 7d70d242f..000000000 --- a/matita/contribs/LAMBDA-TYPES/Level-1/problems-2.ma +++ /dev/null @@ -1,157 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -(* Problematic objects for disambiguation/typechecking ********************) - -set "baseuri" "cic:/matita/LAMBDA-TYPES/Level-1/problems". - -include "LambdaDelta/theory.ma". - -theorem drop1_getl_trans: - \forall (hds: PList).(\forall (c1: C).(\forall (c2: C).((drop1 hds c2 c1) -\to (\forall (b: B).(\forall (e1: C).(\forall (v: T).(\forall (i: nat).((getl -i c1 (CHead e1 (Bind b) v)) \to (ex C (\lambda (e2: C).(getl (trans hds i) c2 -(CHead e2 (Bind b) (ctrans hds i v))))))))))))) -\def - \lambda (hds: PList).(PList_ind (\lambda (p: PList).(\forall (c1: -C).(\forall (c2: C).((drop1 p c2 c1) \to (\forall (b: B).(\forall (e1: -C).(\forall (v: T).(\forall (i: nat).((getl i c1 (CHead e1 (Bind b) v)) \to -(ex C (\lambda (e2: C).(getl (trans p i) c2 (CHead e2 (Bind b) (ctrans p i -v)))))))))))))) (\lambda (c1: C).(\lambda (c2: C).(\lambda (H: (drop1 PNil c2 -c1)).(\lambda (b: B).(\lambda (e1: C).(\lambda (v: T).(\lambda (i: -nat).(\lambda (H0: (getl i c1 (CHead e1 (Bind b) v))).(let H1 \def (match H -in drop1 return (\lambda (p: PList).(\lambda (c: C).(\lambda (c0: C).(\lambda -(_: (drop1 p c c0)).((eq PList p PNil) \to ((eq C c c2) \to ((eq C c0 c1) \to -(ex C (\lambda (e2: C).(getl i c2 (CHead e2 (Bind b) v))))))))))) with -[(drop1_nil c) \Rightarrow (\lambda (_: (eq PList PNil PNil)).(\lambda (H2: -(eq C c c2)).(\lambda (H3: (eq C c c1)).(eq_ind C c2 (\lambda (c0: C).((eq C -c0 c1) \to (ex C (\lambda (e2: C).(getl i c2 (CHead e2 (Bind b) v)))))) -(\lambda (H4: (eq C c2 c1)).(eq_ind C c1 (\lambda (c0: C).(ex C (\lambda (e2: -C).(getl i c0 (CHead e2 (Bind b) v))))) (ex_intro C (\lambda (e2: C).(getl i -c1 (CHead e2 (Bind b) v))) e1 H0) c2 (sym_eq C c2 c1 H4))) c (sym_eq C c c2 -H2) H3)))) | (drop1_cons c0 c3 h d H1 c4 hds H2) \Rightarrow (\lambda (H3: -(eq PList (PCons h d hds) PNil)).(\lambda (H4: (eq C c0 c2)).(\lambda (H5: -(eq C c4 c1)).((let H6 \def (eq_ind PList (PCons h d hds) (\lambda (e: -PList).(match e in PList return (\lambda (_: PList).Prop) with [PNil -\Rightarrow False | (PCons _ _ _) \Rightarrow True])) I PNil H3) in -(False_ind ((eq C c0 c2) \to ((eq C c4 c1) \to ((drop h d c0 c3) \to ((drop1 -hds c3 c4) \to (ex C (\lambda (e2: C).(getl i c2 (CHead e2 (Bind b) v)))))))) -H6)) H4 H5 H1 H2))))]) in (H1 (refl_equal PList PNil) (refl_equal C c2) -(refl_equal C c1))))))))))) (\lambda (h: nat).(\lambda (d: nat).(\lambda -(hds0: PList).(\lambda (H: ((\forall (c1: C).(\forall (c2: C).((drop1 hds0 c2 -c1) \to (\forall (b: B).(\forall (e1: C).(\forall (v: T).(\forall (i: -nat).((getl i c1 (CHead e1 (Bind b) v)) \to (ex C (\lambda (e2: C).(getl -(trans hds0 i) c2 (CHead e2 (Bind b) (ctrans hds0 i v))))))))))))))).(\lambda -(c1: C).(\lambda (c2: C).(\lambda (H0: (drop1 (PCons h d hds0) c2 -c1)).(\lambda (b: B).(\lambda (e1: C).(\lambda (v: T).(\lambda (i: -nat).(\lambda (H1: (getl i c1 (CHead e1 (Bind b) v))).(let H2 \def (match H0 -in drop1 return (\lambda (p: PList).(\lambda (c: C).(\lambda (c0: C).(\lambda -(_: (drop1 p c c0)).((eq PList p (PCons h d hds0)) \to ((eq C c c2) \to ((eq -C c0 c1) \to (ex C (\lambda (e2: C).(getl (match (blt (trans hds0 i) d) with -[true \Rightarrow (trans hds0 i) | false \Rightarrow (plus (trans hds0 i) -h)]) c2 (CHead e2 (Bind b) (match (blt (trans hds0 i) d) with [true -\Rightarrow (lift h (minus d (S (trans hds0 i))) (ctrans hds0 i v)) | false -\Rightarrow (ctrans hds0 i v)])))))))))))) with [(drop1_nil c) \Rightarrow -(\lambda (H2: (eq PList PNil (PCons h d hds0))).(\lambda (H3: (eq C c -c2)).(\lambda (H4: (eq C c c1)).((let H5 \def (eq_ind PList PNil (\lambda (e: -PList).(match e in PList return (\lambda (_: PList).Prop) with [PNil -\Rightarrow True | (PCons _ _ _) \Rightarrow False])) I (PCons h d hds0) H2) -in (False_ind ((eq C c c2) \to ((eq C c c1) \to (ex C (\lambda (e2: C).(getl -(match (blt (trans hds0 i) d) with [true \Rightarrow (trans hds0 i) | false -\Rightarrow (plus (trans hds0 i) h)]) c2 (CHead e2 (Bind b) (match (blt -(trans hds0 i) d) with [true \Rightarrow (lift h (minus d (S (trans hds0 i))) -(ctrans hds0 i v)) | false \Rightarrow (ctrans hds0 i v)]))))))) H5)) H3 -H4)))) | (drop1_cons c0 c3 h0 d0 H2 c4 hds0 H3) \Rightarrow (\lambda (H4: (eq -PList (PCons h0 d0 hds0) (PCons h d hds0))).(\lambda (H5: (eq C c0 -c2)).(\lambda (H6: (eq C c4 c1)).((let H7 \def (f_equal PList PList (\lambda -(e: PList).(match e in PList return (\lambda (_: PList).PList) with [PNil -\Rightarrow hds0 | (PCons _ _ p) \Rightarrow p])) (PCons h0 d0 hds0) (PCons h -d hds0) H4) in ((let H8 \def (f_equal PList nat (\lambda (e: PList).(match e -in PList return (\lambda (_: PList).nat) with [PNil \Rightarrow d0 | (PCons _ -n _) \Rightarrow n])) (PCons h0 d0 hds0) (PCons h d hds0) H4) in ((let H9 -\def (f_equal PList nat (\lambda (e: PList).(match e in PList return (\lambda -(_: PList).nat) with [PNil \Rightarrow h0 | (PCons n _ _) \Rightarrow n])) -(PCons h0 d0 hds0) (PCons h d hds0) H4) in (eq_ind nat h (\lambda (n: -nat).((eq nat d0 d) \to ((eq PList hds0 hds0) \to ((eq C c0 c2) \to ((eq C c4 -c1) \to ((drop n d0 c0 c3) \to ((drop1 hds0 c3 c4) \to (ex C (\lambda (e2: -C).(getl (match (blt (trans hds0 i) d) with [true \Rightarrow (trans hds0 i) -| false \Rightarrow (plus (trans hds0 i) h)]) c2 (CHead e2 (Bind b) (match -(blt (trans hds0 i) d) with [true \Rightarrow (lift h (minus d (S (trans hds0 -i))) (ctrans hds0 i v)) | false \Rightarrow (ctrans hds0 i v)])))))))))))) -(\lambda (H10: (eq nat d0 d)).(eq_ind nat d (\lambda (n: nat).((eq PList hds0 -hds0) \to ((eq C c0 c2) \to ((eq C c4 c1) \to ((drop h n c0 c3) \to ((drop1 -hds0 c3 c4) \to (ex C (\lambda (e2: C).(getl (match (blt (trans hds0 i) d) -with [true \Rightarrow (trans hds0 i) | false \Rightarrow (plus (trans hds0 -i) h)]) c2 (CHead e2 (Bind b) (match (blt (trans hds0 i) d) with [true -\Rightarrow (lift h (minus d (S (trans hds0 i))) (ctrans hds0 i v)) | false -\Rightarrow (ctrans hds0 i v)]))))))))))) (\lambda (H11: (eq PList hds0 -hds0)).(eq_ind PList hds0 (\lambda (p: PList).((eq C c0 c2) \to ((eq C c4 c1) -\to ((drop h d c0 c3) \to ((drop1 p c3 c4) \to (ex C (\lambda (e2: C).(getl -(match (blt (trans hds0 i) d) with [true \Rightarrow (trans hds0 i) | false -\Rightarrow (plus (trans hds0 i) h)]) c2 (CHead e2 (Bind b) (match (blt -(trans hds0 i) d) with [true \Rightarrow (lift h (minus d (S (trans hds0 i))) -(ctrans hds0 i v)) | false \Rightarrow (ctrans hds0 i v)])))))))))) (\lambda -(H12: (eq C c0 c2)).(eq_ind C c2 (\lambda (c: C).((eq C c4 c1) \to ((drop h d -c c3) \to ((drop1 hds0 c3 c4) \to (ex C (\lambda (e2: C).(getl (match (blt -(trans hds0 i) d) with [true \Rightarrow (trans hds0 i) | false \Rightarrow -(plus (trans hds0 i) h)]) c2 (CHead e2 (Bind b) (match (blt (trans hds0 i) d) -with [true \Rightarrow (lift h (minus d (S (trans hds0 i))) (ctrans hds0 i -v)) | false \Rightarrow (ctrans hds0 i v)]))))))))) (\lambda (H13: (eq C c4 -c1)).(eq_ind C c1 (\lambda (c: C).((drop h d c2 c3) \to ((drop1 hds0 c3 c) -\to (ex C (\lambda (e2: C).(getl (match (blt (trans hds0 i) d) with [true -\Rightarrow (trans hds0 i) | false \Rightarrow (plus (trans hds0 i) h)]) c2 -(CHead e2 (Bind b) (match (blt (trans hds0 i) d) with [true \Rightarrow (lift -h (minus d (S (trans hds0 i))) (ctrans hds0 i v)) | false \Rightarrow (ctrans -hds0 i v)])))))))) (\lambda (H14: (drop h d c2 c3)).(\lambda (H15: (drop1 -hds0 c3 c1)).(xinduction bool (blt (trans hds0 i) d) (\lambda (b0: bool).(ex -C (\lambda (e2: C).(getl (match b0 with [true \Rightarrow (trans hds0 i) | -false \Rightarrow (plus (trans hds0 i) h)]) c2 (CHead e2 (Bind b) (match b0 -with [true \Rightarrow (lift h (minus d (S (trans hds0 i))) (ctrans hds0 i -v)) | false \Rightarrow (ctrans hds0 i v)])))))) (\lambda (x_x: -bool).(bool_ind (\lambda (b0: bool).((eq bool (blt (trans hds0 i) d) b0) \to -(ex C (\lambda (e2: C).(getl (match b0 with [true \Rightarrow (trans hds0 i) -| false \Rightarrow (plus (trans hds0 i) h)]) c2 (CHead e2 (Bind b) (match b0 -with [true \Rightarrow (lift h (minus d (S (trans hds0 i))) (ctrans hds0 i -v)) | false \Rightarrow (ctrans hds0 i v)]))))))) (\lambda (H0: (eq bool (blt -(trans hds0 i) d) true)).(let H_x \def (H c1 c3 H15 b e1 v i H1) in (let H16 -\def H_x in (ex_ind C (\lambda (e2: C).(getl (trans hds0 i) c3 (CHead e2 -(Bind b) (ctrans hds0 i v)))) (ex C (\lambda (e2: C).(getl (trans hds0 i) c2 -(CHead e2 (Bind b) (lift h (minus d (S (trans hds0 i))) (ctrans hds0 i -v)))))) (\lambda (x: C).(\lambda (H17: (getl (trans hds0 i) c3 (CHead x (Bind -b) (ctrans hds0 i v)))).(let H_x0 \def (drop_getl_trans_lt (trans hds0 i) d -(le_S_n (S (trans hds0 i)) d (lt_le_S (S (trans hds0 i)) (S d) (blt_lt (S d) -(S (trans hds0 i)) H0))) c2 c3 h H14 b x (ctrans hds0 i v) H17) in (let H -\def H_x0 in (ex2_ind C (\lambda (e1: C).(getl (trans hds0 i) c2 (CHead e1 -(Bind b) (lift h (minus d (S (trans hds0 i))) (ctrans hds0 i v))))) (\lambda -(e1: C).(drop h (minus d (S (trans hds0 i))) e1 x)) (ex C (\lambda (e2: -C).(getl (trans hds0 i) c2 (CHead e2 (Bind b) (lift h (minus d (S (trans hds0 -i))) (ctrans hds0 i v)))))) (\lambda (x0: C).(\lambda (H1: (getl (trans hds0 -i) c2 (CHead x0 (Bind b) (lift h (minus d (S (trans hds0 i))) (ctrans hds0 i -v))))).(\lambda (_: (drop h (minus d (S (trans hds0 i))) x0 x)).(ex_intro C -(\lambda (e2: C).(getl (trans hds0 i) c2 (CHead e2 (Bind b) (lift h (minus d -(S (trans hds0 i))) (ctrans hds0 i v))))) x0 H1)))) H))))) H16)))) (\lambda -(H0: (eq bool (blt (trans hds0 i) d) false)).(let H_x \def (H c1 c3 H15 b e1 -v i H1) in (let H16 \def H_x in (ex_ind C (\lambda (e2: C).(getl (trans hds0 -i) c3 (CHead e2 (Bind b) (ctrans hds0 i v)))) (ex C (\lambda (e2: C).(getl -(plus (trans hds0 i) h) c2 (CHead e2 (Bind b) (ctrans hds0 i v))))) (\lambda -(x: C).(\lambda (H17: (getl (trans hds0 i) c3 (CHead x (Bind b) (ctrans hds0 -i v)))).(let H \def (drop_getl_trans_ge (trans hds0 i) c2 c3 d h H14 (CHead x -(Bind b) (ctrans hds0 i v)) H17) in (ex_intro C (\lambda (e2: C).(getl (plus -(trans hds0 i) h) c2 (CHead e2 (Bind b) (ctrans hds0 i v)))) x (H (bge_le d -(trans hds0 i) H0)))))) H16)))) x_x))))) c4 (sym_eq C c4 c1 H13))) c0 (sym_eq -C c0 c2 H12))) hds0 (sym_eq PList hds0 hds0 H11))) d0 (sym_eq nat d0 d H10))) -h0 (sym_eq nat h0 h H9))) H8)) H7)) H5 H6 H2 H3))))]) in (H2 (refl_equal -PList (PCons h d hds0)) (refl_equal C c2) (refl_equal C c1))))))))))))))) -hds). - diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/problems-3.ma b/matita/contribs/LAMBDA-TYPES/Level-1/problems-3.ma deleted file mode 100644 index b4020afb8..000000000 --- a/matita/contribs/LAMBDA-TYPES/Level-1/problems-3.ma +++ /dev/null @@ -1,396 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -(* Problematic objects for disambiguation/typechecking ********************) - -set "baseuri" "cic:/matita/LAMBDA-TYPES/Level-1/problems". - -include "LambdaDelta/theory.ma". - -theorem asucc_inj: - \forall (g: G).(\forall (a1: A).(\forall (a2: A).((leq g (asucc g a1) (asucc -g a2)) \to (leq g a1 a2)))) -\def - \lambda (g: G).(\lambda (a1: A).(A_ind (\lambda (a: A).(\forall (a2: -A).((leq g (asucc g a) (asucc g a2)) \to (leq g a a2)))) (\lambda (n: -nat).(\lambda (n0: nat).(\lambda (a2: A).(A_ind (\lambda (a: A).((leq g -(asucc g (ASort n n0)) (asucc g a)) \to (leq g (ASort n n0) a))) (\lambda -(n1: nat).(\lambda (n2: nat).(\lambda (H: (leq g (asucc g (ASort n n0)) -(asucc g (ASort n1 n2)))).((match n in nat return (\lambda (n3: nat).((leq g -(asucc g (ASort n3 n0)) (asucc g (ASort n1 n2))) \to (leq g (ASort n3 n0) -(ASort n1 n2)))) with [O \Rightarrow (\lambda (H0: (leq g (asucc g (ASort O -n0)) (asucc g (ASort n1 n2)))).((match n1 in nat return (\lambda (n3: -nat).((leq g (asucc g (ASort O n0)) (asucc g (ASort n3 n2))) \to (leq g -(ASort O n0) (ASort n3 n2)))) with [O \Rightarrow (\lambda (H1: (leq g (asucc -g (ASort O n0)) (asucc g (ASort O n2)))).(let H2 \def (match H1 in leq return -(\lambda (a: A).(\lambda (a0: A).(\lambda (_: (leq ? a a0)).((eq A a (ASort O -(next g n0))) \to ((eq A a0 (ASort O (next g n2))) \to (leq g (ASort O n0) -(ASort O n2))))))) with [(leq_sort h1 h2 n1 n3 k H0) \Rightarrow (\lambda -(H1: (eq A (ASort h1 n1) (ASort O (next g n0)))).(\lambda (H2: (eq A (ASort -h2 n3) (ASort O (next g n2)))).((let H3 \def (f_equal A nat (\lambda (e: -A).(match e in A return (\lambda (_: A).nat) with [(ASort _ n) \Rightarrow n -| (AHead _ _) \Rightarrow n1])) (ASort h1 n1) (ASort O (next g n0)) H1) in -((let H4 \def (f_equal A nat (\lambda (e: A).(match e in A return (\lambda -(_: A).nat) with [(ASort n _) \Rightarrow n | (AHead _ _) \Rightarrow h1])) -(ASort h1 n1) (ASort O (next g n0)) H1) in (eq_ind nat O (\lambda (n: -nat).((eq nat n1 (next g n0)) \to ((eq A (ASort h2 n3) (ASort O (next g n2))) -\to ((eq A (aplus g (ASort n n1) k) (aplus g (ASort h2 n3) k)) \to (leq g -(ASort O n0) (ASort O n2)))))) (\lambda (H5: (eq nat n1 (next g n0))).(eq_ind -nat (next g n0) (\lambda (n: nat).((eq A (ASort h2 n3) (ASort O (next g n2))) -\to ((eq A (aplus g (ASort O n) k) (aplus g (ASort h2 n3) k)) \to (leq g -(ASort O n0) (ASort O n2))))) (\lambda (H6: (eq A (ASort h2 n3) (ASort O -(next g n2)))).(let H7 \def (f_equal A nat (\lambda (e: A).(match e in A -return (\lambda (_: A).nat) with [(ASort _ n) \Rightarrow n | (AHead _ _) -\Rightarrow n3])) (ASort h2 n3) (ASort O (next g n2)) H6) in ((let H8 \def -(f_equal A nat (\lambda (e: A).(match e in A return (\lambda (_: A).nat) with -[(ASort n _) \Rightarrow n | (AHead _ _) \Rightarrow h2])) (ASort h2 n3) -(ASort O (next g n2)) H6) in (eq_ind nat O (\lambda (n: nat).((eq nat n3 -(next g n2)) \to ((eq A (aplus g (ASort O (next g n0)) k) (aplus g (ASort n -n3) k)) \to (leq g (ASort O n0) (ASort O n2))))) (\lambda (H9: (eq nat n3 -(next g n2))).(eq_ind nat (next g n2) (\lambda (n: nat).((eq A (aplus g -(ASort O (next g n0)) k) (aplus g (ASort O n) k)) \to (leq g (ASort O n0) -(ASort O n2)))) (\lambda (H10: (eq A (aplus g (ASort O (next g n0)) k) (aplus -g (ASort O (next g n2)) k))).(let H \def (eq_ind_r A (aplus g (ASort O (next -g n0)) k) (\lambda (a: A).(eq A a (aplus g (ASort O (next g n2)) k))) H10 -(aplus g (ASort O n0) (S k)) (aplus_sort_O_S_simpl g n0 k)) in (let H11 \def -(eq_ind_r A (aplus g (ASort O (next g n2)) k) (\lambda (a: A).(eq A (aplus g -(ASort O n0) (S k)) a)) H (aplus g (ASort O n2) (S k)) (aplus_sort_O_S_simpl -g n2 k)) in (leq_sort g O O n0 n2 (S k) H11)))) n3 (sym_eq nat n3 (next g n2) -H9))) h2 (sym_eq nat h2 O H8))) H7))) n1 (sym_eq nat n1 (next g n0) H5))) h1 -(sym_eq nat h1 O H4))) H3)) H2 H0))) | (leq_head a1 a2 H0 a3 a4 H1) -\Rightarrow (\lambda (H2: (eq A (AHead a1 a3) (ASort O (next g -n0)))).(\lambda (H3: (eq A (AHead a2 a4) (ASort O (next g n2)))).((let H4 -\def (eq_ind A (AHead a1 a3) (\lambda (e: A).(match e in A return (\lambda -(_: A).Prop) with [(ASort _ _) \Rightarrow False | (AHead _ _) \Rightarrow -True])) I (ASort O (next g n0)) H2) in (False_ind ((eq A (AHead a2 a4) (ASort -O (next g n2))) \to ((leq g a1 a2) \to ((leq g a3 a4) \to (leq g (ASort O n0) -(ASort O n2))))) H4)) H3 H0 H1)))]) in (H2 (refl_equal A (ASort O (next g -n0))) (refl_equal A (ASort O (next g n2)))))) | (S n3) \Rightarrow (\lambda -(H1: (leq g (asucc g (ASort O n0)) (asucc g (ASort (S n3) n2)))).(let H2 \def -(match H1 in leq return (\lambda (a: A).(\lambda (a0: A).(\lambda (_: (leq ? -a a0)).((eq A a (ASort O (next g n0))) \to ((eq A a0 (ASort n3 n2)) \to (leq -g (ASort O n0) (ASort (S n3) n2))))))) with [(leq_sort h1 h2 n1 n3 k H0) -\Rightarrow (\lambda (H1: (eq A (ASort h1 n1) (ASort O (next g -n0)))).(\lambda (H2: (eq A (ASort h2 n3) (ASort n3 n2))).((let H3 \def -(f_equal A nat (\lambda (e: A).(match e in A return (\lambda (_: A).nat) with -[(ASort _ n) \Rightarrow n | (AHead _ _) \Rightarrow n1])) (ASort h1 n1) -(ASort O (next g n0)) H1) in ((let H4 \def (f_equal A nat (\lambda (e: -A).(match e in A return (\lambda (_: A).nat) with [(ASort n _) \Rightarrow n -| (AHead _ _) \Rightarrow h1])) (ASort h1 n1) (ASort O (next g n0)) H1) in -(eq_ind nat O (\lambda (n: nat).((eq nat n1 (next g n0)) \to ((eq A (ASort h2 -n3) (ASort n3 n2)) \to ((eq A (aplus g (ASort n n1) k) (aplus g (ASort h2 n3) -k)) \to (leq g (ASort O n0) (ASort (S n3) n2)))))) (\lambda (H5: (eq nat n1 -(next g n0))).(eq_ind nat (next g n0) (\lambda (n: nat).((eq A (ASort h2 n3) -(ASort n3 n2)) \to ((eq A (aplus g (ASort O n) k) (aplus g (ASort h2 n3) k)) -\to (leq g (ASort O n0) (ASort (S n3) n2))))) (\lambda (H6: (eq A (ASort h2 -n3) (ASort n3 n2))).(let H7 \def (f_equal A nat (\lambda (e: A).(match e in A -return (\lambda (_: A).nat) with [(ASort _ n) \Rightarrow n | (AHead _ _) -\Rightarrow n3])) (ASort h2 n3) (ASort n3 n2) H6) in ((let H8 \def (f_equal A -nat (\lambda (e: A).(match e in A return (\lambda (_: A).nat) with [(ASort n -_) \Rightarrow n | (AHead _ _) \Rightarrow h2])) (ASort h2 n3) (ASort n3 n2) -H6) in (eq_ind nat n3 (\lambda (n: nat).((eq nat n3 n2) \to ((eq A (aplus g -(ASort O (next g n0)) k) (aplus g (ASort n n3) k)) \to (leq g (ASort O n0) -(ASort (S n3) n2))))) (\lambda (H9: (eq nat n3 n2)).(eq_ind nat n2 (\lambda -(n: nat).((eq A (aplus g (ASort O (next g n0)) k) (aplus g (ASort n3 n) k)) -\to (leq g (ASort O n0) (ASort (S n3) n2)))) (\lambda (H10: (eq A (aplus g -(ASort O (next g n0)) k) (aplus g (ASort n3 n2) k))).(let H \def (eq_ind_r A -(aplus g (ASort O (next g n0)) k) (\lambda (a: A).(eq A a (aplus g (ASort n3 -n2) k))) H10 (aplus g (ASort O n0) (S k)) (aplus_sort_O_S_simpl g n0 k)) in -(let H11 \def (eq_ind_r A (aplus g (ASort n3 n2) k) (\lambda (a: A).(eq A -(aplus g (ASort O n0) (S k)) a)) H (aplus g (ASort (S n3) n2) (S k)) -(aplus_sort_S_S_simpl g n2 n3 k)) in (leq_sort g O (S n3) n0 n2 (S k) H11)))) -n3 (sym_eq nat n3 n2 H9))) h2 (sym_eq nat h2 n3 H8))) H7))) n1 (sym_eq nat n1 -(next g n0) H5))) h1 (sym_eq nat h1 O H4))) H3)) H2 H0))) | (leq_head a1 a2 -H0 a3 a4 H1) \Rightarrow (\lambda (H2: (eq A (AHead a1 a3) (ASort O (next g -n0)))).(\lambda (H3: (eq A (AHead a2 a4) (ASort n3 n2))).((let H4 \def -(eq_ind A (AHead a1 a3) (\lambda (e: A).(match e in A return (\lambda (_: -A).Prop) with [(ASort _ _) \Rightarrow False | (AHead _ _) \Rightarrow -True])) I (ASort O (next g n0)) H2) in (False_ind ((eq A (AHead a2 a4) (ASort -n3 n2)) \to ((leq g a1 a2) \to ((leq g a3 a4) \to (leq g (ASort O n0) (ASort -(S n3) n2))))) H4)) H3 H0 H1)))]) in (H2 (refl_equal A (ASort O (next g n0))) -(refl_equal A (ASort n3 n2)))))]) H0)) | (S n3) \Rightarrow (\lambda (H0: -(leq g (asucc g (ASort (S n3) n0)) (asucc g (ASort n1 n2)))).((match n1 in -nat return (\lambda (n4: nat).((leq g (asucc g (ASort (S n3) n0)) (asucc g -(ASort n4 n2))) \to (leq g (ASort (S n3) n0) (ASort n4 n2)))) with [O -\Rightarrow (\lambda (H1: (leq g (asucc g (ASort (S n3) n0)) (asucc g (ASort -O n2)))).(let H2 \def (match H1 in leq return (\lambda (a: A).(\lambda (a0: -A).(\lambda (_: (leq ? a a0)).((eq A a (ASort n3 n0)) \to ((eq A a0 (ASort O -(next g n2))) \to (leq g (ASort (S n3) n0) (ASort O n2))))))) with [(leq_sort -h1 h2 n1 n3 k H0) \Rightarrow (\lambda (H1: (eq A (ASort h1 n1) (ASort n3 -n0))).(\lambda (H2: (eq A (ASort h2 n3) (ASort O (next g n2)))).((let H3 \def -(f_equal A nat (\lambda (e: A).(match e in A return (\lambda (_: A).nat) with -[(ASort _ n) \Rightarrow n | (AHead _ _) \Rightarrow n1])) (ASort h1 n1) -(ASort n3 n0) H1) in ((let H4 \def (f_equal A nat (\lambda (e: A).(match e in -A return (\lambda (_: A).nat) with [(ASort n _) \Rightarrow n | (AHead _ _) -\Rightarrow h1])) (ASort h1 n1) (ASort n3 n0) H1) in (eq_ind nat n3 (\lambda -(n: nat).((eq nat n1 n0) \to ((eq A (ASort h2 n3) (ASort O (next g n2))) \to -((eq A (aplus g (ASort n n1) k) (aplus g (ASort h2 n3) k)) \to (leq g (ASort -(S n3) n0) (ASort O n2)))))) (\lambda (H5: (eq nat n1 n0)).(eq_ind nat n0 -(\lambda (n: nat).((eq A (ASort h2 n3) (ASort O (next g n2))) \to ((eq A -(aplus g (ASort n3 n) k) (aplus g (ASort h2 n3) k)) \to (leq g (ASort (S n3) -n0) (ASort O n2))))) (\lambda (H6: (eq A (ASort h2 n3) (ASort O (next g -n2)))).(let H7 \def (f_equal A nat (\lambda (e: A).(match e in A return -(\lambda (_: A).nat) with [(ASort _ n) \Rightarrow n | (AHead _ _) -\Rightarrow n3])) (ASort h2 n3) (ASort O (next g n2)) H6) in ((let H8 \def -(f_equal A nat (\lambda (e: A).(match e in A return (\lambda (_: A).nat) with -[(ASort n _) \Rightarrow n | (AHead _ _) \Rightarrow h2])) (ASort h2 n3) -(ASort O (next g n2)) H6) in (eq_ind nat O (\lambda (n: nat).((eq nat n3 -(next g n2)) \to ((eq A (aplus g (ASort n3 n0) k) (aplus g (ASort n n3) k)) -\to (leq g (ASort (S n3) n0) (ASort O n2))))) (\lambda (H9: (eq nat n3 (next -g n2))).(eq_ind nat (next g n2) (\lambda (n: nat).((eq A (aplus g (ASort n3 -n0) k) (aplus g (ASort O n) k)) \to (leq g (ASort (S n3) n0) (ASort O n2)))) -(\lambda (H10: (eq A (aplus g (ASort n3 n0) k) (aplus g (ASort O (next g n2)) -k))).(let H \def (eq_ind_r A (aplus g (ASort n3 n0) k) (\lambda (a: A).(eq A -a (aplus g (ASort O (next g n2)) k))) H10 (aplus g (ASort (S n3) n0) (S k)) -(aplus_sort_S_S_simpl g n0 n3 k)) in (let H11 \def (eq_ind_r A (aplus g -(ASort O (next g n2)) k) (\lambda (a: A).(eq A (aplus g (ASort (S n3) n0) (S -k)) a)) H (aplus g (ASort O n2) (S k)) (aplus_sort_O_S_simpl g n2 k)) in -(leq_sort g (S n3) O n0 n2 (S k) H11)))) n3 (sym_eq nat n3 (next g n2) H9))) -h2 (sym_eq nat h2 O H8))) H7))) n1 (sym_eq nat n1 n0 H5))) h1 (sym_eq nat h1 -n3 H4))) H3)) H2 H0))) | (leq_head a1 a2 H0 a3 a4 H1) \Rightarrow (\lambda -(H2: (eq A (AHead a1 a3) (ASort n3 n0))).(\lambda (H3: (eq A (AHead a2 a4) -(ASort O (next g n2)))).((let H4 \def (eq_ind A (AHead a1 a3) (\lambda (e: -A).(match e in A return (\lambda (_: A).Prop) with [(ASort _ _) \Rightarrow -False | (AHead _ _) \Rightarrow True])) I (ASort n3 n0) H2) in (False_ind -((eq A (AHead a2 a4) (ASort O (next g n2))) \to ((leq g a1 a2) \to ((leq g a3 -a4) \to (leq g (ASort (S n3) n0) (ASort O n2))))) H4)) H3 H0 H1)))]) in (H2 -(refl_equal A (ASort n3 n0)) (refl_equal A (ASort O (next g n2)))))) | (S n4) -\Rightarrow (\lambda (H1: (leq g (asucc g (ASort (S n3) n0)) (asucc g (ASort -(S n4) n2)))).(let H2 \def (match H1 in leq return (\lambda (a: A).(\lambda -(a0: A).(\lambda (_: (leq ? a a0)).((eq A a (ASort n3 n0)) \to ((eq A a0 -(ASort n4 n2)) \to (leq g (ASort (S n3) n0) (ASort (S n4) n2))))))) with -[(leq_sort h1 h2 n3 n4 k H0) \Rightarrow (\lambda (H1: (eq A (ASort h1 n3) -(ASort n3 n0))).(\lambda (H2: (eq A (ASort h2 n4) (ASort n4 n2))).((let H3 -\def (f_equal A nat (\lambda (e: A).(match e in A return (\lambda (_: A).nat) -with [(ASort _ n) \Rightarrow n | (AHead _ _) \Rightarrow n3])) (ASort h1 n3) -(ASort n3 n0) H1) in ((let H4 \def (f_equal A nat (\lambda (e: A).(match e in -A return (\lambda (_: A).nat) with [(ASort n _) \Rightarrow n | (AHead _ _) -\Rightarrow h1])) (ASort h1 n3) (ASort n3 n0) H1) in (eq_ind nat n3 (\lambda -(n: nat).((eq nat n3 n0) \to ((eq A (ASort h2 n4) (ASort n4 n2)) \to ((eq A -(aplus g (ASort n n3) k) (aplus g (ASort h2 n4) k)) \to (leq g (ASort (S n3) -n0) (ASort (S n4) n2)))))) (\lambda (H5: (eq nat n3 n0)).(eq_ind nat n0 -(\lambda (n: nat).((eq A (ASort h2 n4) (ASort n4 n2)) \to ((eq A (aplus g -(ASort n3 n) k) (aplus g (ASort h2 n4) k)) \to (leq g (ASort (S n3) n0) -(ASort (S n4) n2))))) (\lambda (H6: (eq A (ASort h2 n4) (ASort n4 n2))).(let -H7 \def (f_equal A nat (\lambda (e: A).(match e in A return (\lambda (_: -A).nat) with [(ASort _ n) \Rightarrow n | (AHead _ _) \Rightarrow n4])) -(ASort h2 n4) (ASort n4 n2) H6) in ((let H8 \def (f_equal A nat (\lambda (e: -A).(match e in A return (\lambda (_: A).nat) with [(ASort n _) \Rightarrow n -| (AHead _ _) \Rightarrow h2])) (ASort h2 n4) (ASort n4 n2) H6) in (eq_ind -nat n4 (\lambda (n: nat).((eq nat n4 n2) \to ((eq A (aplus g (ASort n3 n0) k) -(aplus g (ASort n n4) k)) \to (leq g (ASort (S n3) n0) (ASort (S n4) n2))))) -(\lambda (H9: (eq nat n4 n2)).(eq_ind nat n2 (\lambda (n: nat).((eq A (aplus -g (ASort n3 n0) k) (aplus g (ASort n4 n) k)) \to (leq g (ASort (S n3) n0) -(ASort (S n4) n2)))) (\lambda (H10: (eq A (aplus g (ASort n3 n0) k) (aplus g -(ASort n4 n2) k))).(let H \def (eq_ind_r A (aplus g (ASort n3 n0) k) (\lambda -(a: A).(eq A a (aplus g (ASort n4 n2) k))) H10 (aplus g (ASort (S n3) n0) (S -k)) (aplus_sort_S_S_simpl g n0 n3 k)) in (let H11 \def (eq_ind_r A (aplus g -(ASort n4 n2) k) (\lambda (a: A).(eq A (aplus g (ASort (S n3) n0) (S k)) a)) -H (aplus g (ASort (S n4) n2) (S k)) (aplus_sort_S_S_simpl g n2 n4 k)) in -(leq_sort g (S n3) (S n4) n0 n2 (S k) H11)))) n4 (sym_eq nat n4 n2 H9))) h2 -(sym_eq nat h2 n4 H8))) H7))) n3 (sym_eq nat n3 n0 H5))) h1 (sym_eq nat h1 n3 -H4))) H3)) H2 H0))) | (leq_head a1 a2 H0 a3 a4 H1) \Rightarrow (\lambda (H2: -(eq A (AHead a1 a3) (ASort n3 n0))).(\lambda (H3: (eq A (AHead a2 a4) (ASort -n4 n2))).((let H4 \def (eq_ind A (AHead a1 a3) (\lambda (e: A).(match e in A -return (\lambda (_: A).Prop) with [(ASort _ _) \Rightarrow False | (AHead _ -_) \Rightarrow True])) I (ASort n3 n0) H2) in (False_ind ((eq A (AHead a2 a4) -(ASort n4 n2)) \to ((leq g a1 a2) \to ((leq g a3 a4) \to (leq g (ASort (S n3) -n0) (ASort (S n4) n2))))) H4)) H3 H0 H1)))]) in (H2 (refl_equal A (ASort n3 -n0)) (refl_equal A (ASort n4 n2)))))]) H0))]) H)))) (\lambda (a: A).(\lambda -(H: (((leq g (asucc g (ASort n n0)) (asucc g a)) \to (leq g (ASort n n0) -a)))).(\lambda (a0: A).(\lambda (H0: (((leq g (asucc g (ASort n n0)) (asucc g -a0)) \to (leq g (ASort n n0) a0)))).(\lambda (H1: (leq g (asucc g (ASort n -n0)) (asucc g (AHead a a0)))).((match n in nat return (\lambda (n1: -nat).((((leq g (asucc g (ASort n1 n0)) (asucc g a)) \to (leq g (ASort n1 n0) -a))) \to ((((leq g (asucc g (ASort n1 n0)) (asucc g a0)) \to (leq g (ASort n1 -n0) a0))) \to ((leq g (asucc g (ASort n1 n0)) (asucc g (AHead a a0))) \to -(leq g (ASort n1 n0) (AHead a a0)))))) with [O \Rightarrow (\lambda (_: -(((leq g (asucc g (ASort O n0)) (asucc g a)) \to (leq g (ASort O n0) -a)))).(\lambda (_: (((leq g (asucc g (ASort O n0)) (asucc g a0)) \to (leq g -(ASort O n0) a0)))).(\lambda (H4: (leq g (asucc g (ASort O n0)) (asucc g -(AHead a a0)))).(let H5 \def (match H4 in leq return (\lambda (a1: -A).(\lambda (a2: A).(\lambda (_: (leq ? a1 a2)).((eq A a1 (ASort O (next g -n0))) \to ((eq A a2 (AHead a (asucc g a0))) \to (leq g (ASort O n0) (AHead a -a0))))))) with [(leq_sort h1 h2 n1 n2 k H2) \Rightarrow (\lambda (H3: (eq A -(ASort h1 n1) (ASort O (next g n0)))).(\lambda (H4: (eq A (ASort h2 n2) -(AHead a (asucc g a0)))).((let H5 \def (f_equal A nat (\lambda (e: A).(match -e in A return (\lambda (_: A).nat) with [(ASort _ n) \Rightarrow n | (AHead _ -_) \Rightarrow n1])) (ASort h1 n1) (ASort O (next g n0)) H3) in ((let H6 \def -(f_equal A nat (\lambda (e: A).(match e in A return (\lambda (_: A).nat) with -[(ASort n _) \Rightarrow n | (AHead _ _) \Rightarrow h1])) (ASort h1 n1) -(ASort O (next g n0)) H3) in (eq_ind nat O (\lambda (n: nat).((eq nat n1 -(next g n0)) \to ((eq A (ASort h2 n2) (AHead a (asucc g a0))) \to ((eq A -(aplus g (ASort n n1) k) (aplus g (ASort h2 n2) k)) \to (leq g (ASort O n0) -(AHead a a0)))))) (\lambda (H7: (eq nat n1 (next g n0))).(eq_ind nat (next g -n0) (\lambda (n: nat).((eq A (ASort h2 n2) (AHead a (asucc g a0))) \to ((eq A -(aplus g (ASort O n) k) (aplus g (ASort h2 n2) k)) \to (leq g (ASort O n0) -(AHead a a0))))) (\lambda (H8: (eq A (ASort h2 n2) (AHead a (asucc g -a0)))).(let H9 \def (eq_ind A (ASort h2 n2) (\lambda (e: A).(match e in A -return (\lambda (_: A).Prop) with [(ASort _ _) \Rightarrow True | (AHead _ _) -\Rightarrow False])) I (AHead a (asucc g a0)) H8) in (False_ind ((eq A (aplus -g (ASort O (next g n0)) k) (aplus g (ASort h2 n2) k)) \to (leq g (ASort O n0) -(AHead a a0))) H9))) n1 (sym_eq nat n1 (next g n0) H7))) h1 (sym_eq nat h1 O -H6))) H5)) H4 H2))) | (leq_head a1 a2 H2 a3 a4 H3) \Rightarrow (\lambda (H4: -(eq A (AHead a1 a3) (ASort O (next g n0)))).(\lambda (H5: (eq A (AHead a2 a4) -(AHead a (asucc g a0)))).((let H6 \def (eq_ind A (AHead a1 a3) (\lambda (e: -A).(match e in A return (\lambda (_: A).Prop) with [(ASort _ _) \Rightarrow -False | (AHead _ _) \Rightarrow True])) I (ASort O (next g n0)) H4) in -(False_ind ((eq A (AHead a2 a4) (AHead a (asucc g a0))) \to ((leq g a1 a2) -\to ((leq g a3 a4) \to (leq g (ASort O n0) (AHead a a0))))) H6)) H5 H2 -H3)))]) in (H5 (refl_equal A (ASort O (next g n0))) (refl_equal A (AHead a -(asucc g a0)))))))) | (S n1) \Rightarrow (\lambda (_: (((leq g (asucc g -(ASort (S n1) n0)) (asucc g a)) \to (leq g (ASort (S n1) n0) a)))).(\lambda -(_: (((leq g (asucc g (ASort (S n1) n0)) (asucc g a0)) \to (leq g (ASort (S -n1) n0) a0)))).(\lambda (H4: (leq g (asucc g (ASort (S n1) n0)) (asucc g -(AHead a a0)))).(let H5 \def (match H4 in leq return (\lambda (a1: -A).(\lambda (a2: A).(\lambda (_: (leq ? a1 a2)).((eq A a1 (ASort n1 n0)) \to -((eq A a2 (AHead a (asucc g a0))) \to (leq g (ASort (S n1) n0) (AHead a -a0))))))) with [(leq_sort h1 h2 n1 n2 k H2) \Rightarrow (\lambda (H3: (eq A -(ASort h1 n1) (ASort n1 n0))).(\lambda (H4: (eq A (ASort h2 n2) (AHead a -(asucc g a0)))).((let H5 \def (f_equal A nat (\lambda (e: A).(match e in A -return (\lambda (_: A).nat) with [(ASort _ n) \Rightarrow n | (AHead _ _) -\Rightarrow n1])) (ASort h1 n1) (ASort n1 n0) H3) in ((let H6 \def (f_equal A -nat (\lambda (e: A).(match e in A return (\lambda (_: A).nat) with [(ASort n -_) \Rightarrow n | (AHead _ _) \Rightarrow h1])) (ASort h1 n1) (ASort n1 n0) -H3) in (eq_ind nat n1 (\lambda (n: nat).((eq nat n1 n0) \to ((eq A (ASort h2 -n2) (AHead a (asucc g a0))) \to ((eq A (aplus g (ASort n n1) k) (aplus g -(ASort h2 n2) k)) \to (leq g (ASort (S n1) n0) (AHead a a0)))))) (\lambda -(H7: (eq nat n1 n0)).(eq_ind nat n0 (\lambda (n: nat).((eq A (ASort h2 n2) -(AHead a (asucc g a0))) \to ((eq A (aplus g (ASort n1 n) k) (aplus g (ASort -h2 n2) k)) \to (leq g (ASort (S n1) n0) (AHead a a0))))) (\lambda (H8: (eq A -(ASort h2 n2) (AHead a (asucc g a0)))).(let H9 \def (eq_ind A (ASort h2 n2) -(\lambda (e: A).(match e in A return (\lambda (_: A).Prop) with [(ASort _ _) -\Rightarrow True | (AHead _ _) \Rightarrow False])) I (AHead a (asucc g a0)) -H8) in (False_ind ((eq A (aplus g (ASort n1 n0) k) (aplus g (ASort h2 n2) k)) -\to (leq g (ASort (S n1) n0) (AHead a a0))) H9))) n1 (sym_eq nat n1 n0 H7))) -h1 (sym_eq nat h1 n1 H6))) H5)) H4 H2))) | (leq_head a1 a2 H2 a3 a4 H3) -\Rightarrow (\lambda (H4: (eq A (AHead a1 a3) (ASort n1 n0))).(\lambda (H5: -(eq A (AHead a2 a4) (AHead a (asucc g a0)))).((let H6 \def (eq_ind A (AHead -a1 a3) (\lambda (e: A).(match e in A return (\lambda (_: A).Prop) with -[(ASort _ _) \Rightarrow False | (AHead _ _) \Rightarrow True])) I (ASort n1 -n0) H4) in (False_ind ((eq A (AHead a2 a4) (AHead a (asucc g a0))) \to ((leq -g a1 a2) \to ((leq g a3 a4) \to (leq g (ASort (S n1) n0) (AHead a a0))))) -H6)) H5 H2 H3)))]) in (H5 (refl_equal A (ASort n1 n0)) (refl_equal A (AHead a -(asucc g a0))))))))]) H H0 H1)))))) a2)))) (\lambda (a: A).(\lambda (_: -((\forall (a2: A).((leq g (asucc g a) (asucc g a2)) \to (leq g a -a2))))).(\lambda (a0: A).(\lambda (H0: ((\forall (a2: A).((leq g (asucc g a0) -(asucc g a2)) \to (leq g a0 a2))))).(\lambda (a2: A).(A_ind (\lambda (a3: -A).((leq g (asucc g (AHead a a0)) (asucc g a3)) \to (leq g (AHead a a0) a3))) -(\lambda (n: nat).(\lambda (n0: nat).(\lambda (H1: (leq g (asucc g (AHead a -a0)) (asucc g (ASort n n0)))).((match n in nat return (\lambda (n1: -nat).((leq g (asucc g (AHead a a0)) (asucc g (ASort n1 n0))) \to (leq g -(AHead a a0) (ASort n1 n0)))) with [O \Rightarrow (\lambda (H2: (leq g (asucc -g (AHead a a0)) (asucc g (ASort O n0)))).(let H3 \def (match H2 in leq return -(\lambda (a1: A).(\lambda (a2: A).(\lambda (_: (leq ? a1 a2)).((eq A a1 -(AHead a (asucc g a0))) \to ((eq A a2 (ASort O (next g n0))) \to (leq g -(AHead a a0) (ASort O n0))))))) with [(leq_sort h1 h2 n1 n2 k H2) \Rightarrow -(\lambda (H3: (eq A (ASort h1 n1) (AHead a (asucc g a0)))).(\lambda (H4: (eq -A (ASort h2 n2) (ASort O (next g n0)))).((let H5 \def (eq_ind A (ASort h1 n1) -(\lambda (e: A).(match e in A return (\lambda (_: A).Prop) with [(ASort _ _) -\Rightarrow True | (AHead _ _) \Rightarrow False])) I (AHead a (asucc g a0)) -H3) in (False_ind ((eq A (ASort h2 n2) (ASort O (next g n0))) \to ((eq A -(aplus g (ASort h1 n1) k) (aplus g (ASort h2 n2) k)) \to (leq g (AHead a a0) -(ASort O n0)))) H5)) H4 H2))) | (leq_head a1 a2 H2 a3 a4 H3) \Rightarrow -(\lambda (H4: (eq A (AHead a1 a3) (AHead a (asucc g a0)))).(\lambda (H5: (eq -A (AHead a2 a4) (ASort O (next g n0)))).((let H6 \def (f_equal A A (\lambda -(e: A).(match e in A return (\lambda (_: A).A) with [(ASort _ _) \Rightarrow -a3 | (AHead _ a) \Rightarrow a])) (AHead a1 a3) (AHead a (asucc g a0)) H4) in -((let H7 \def (f_equal A A (\lambda (e: A).(match e in A return (\lambda (_: -A).A) with [(ASort _ _) \Rightarrow a1 | (AHead a _) \Rightarrow a])) (AHead -a1 a3) (AHead a (asucc g a0)) H4) in (eq_ind A a (\lambda (a5: A).((eq A a3 -(asucc g a0)) \to ((eq A (AHead a2 a4) (ASort O (next g n0))) \to ((leq g a5 -a2) \to ((leq g a3 a4) \to (leq g (AHead a a0) (ASort O n0))))))) (\lambda -(H8: (eq A a3 (asucc g a0))).(eq_ind A (asucc g a0) (\lambda (a5: A).((eq A -(AHead a2 a4) (ASort O (next g n0))) \to ((leq g a a2) \to ((leq g a5 a4) \to -(leq g (AHead a a0) (ASort O n0)))))) (\lambda (H9: (eq A (AHead a2 a4) -(ASort O (next g n0)))).(let H10 \def (eq_ind A (AHead a2 a4) (\lambda (e: -A).(match e in A return (\lambda (_: A).Prop) with [(ASort _ _) \Rightarrow -False | (AHead _ _) \Rightarrow True])) I (ASort O (next g n0)) H9) in -(False_ind ((leq g a a2) \to ((leq g (asucc g a0) a4) \to (leq g (AHead a a0) -(ASort O n0)))) H10))) a3 (sym_eq A a3 (asucc g a0) H8))) a1 (sym_eq A a1 a -H7))) H6)) H5 H2 H3)))]) in (H3 (refl_equal A (AHead a (asucc g a0))) -(refl_equal A (ASort O (next g n0)))))) | (S n1) \Rightarrow (\lambda (H2: -(leq g (asucc g (AHead a a0)) (asucc g (ASort (S n1) n0)))).(let H3 \def -(match H2 in leq return (\lambda (a1: A).(\lambda (a2: A).(\lambda (_: (leq ? -a1 a2)).((eq A a1 (AHead a (asucc g a0))) \to ((eq A a2 (ASort n1 n0)) \to -(leq g (AHead a a0) (ASort (S n1) n0))))))) with [(leq_sort h1 h2 n1 n2 k H2) -\Rightarrow (\lambda (H3: (eq A (ASort h1 n1) (AHead a (asucc g -a0)))).(\lambda (H4: (eq A (ASort h2 n2) (ASort n1 n0))).((let H5 \def -(eq_ind A (ASort h1 n1) (\lambda (e: A).(match e in A return (\lambda (_: -A).Prop) with [(ASort _ _) \Rightarrow True | (AHead _ _) \Rightarrow -False])) I (AHead a (asucc g a0)) H3) in (False_ind ((eq A (ASort h2 n2) -(ASort n1 n0)) \to ((eq A (aplus g (ASort h1 n1) k) (aplus g (ASort h2 n2) -k)) \to (leq g (AHead a a0) (ASort (S n1) n0)))) H5)) H4 H2))) | (leq_head a1 -a2 H2 a3 a4 H3) \Rightarrow (\lambda (H4: (eq A (AHead a1 a3) (AHead a (asucc -g a0)))).(\lambda (H5: (eq A (AHead a2 a4) (ASort n1 n0))).((let H6 \def -(f_equal A A (\lambda (e: A).(match e in A return (\lambda (_: A).A) with -[(ASort _ _) \Rightarrow a3 | (AHead _ a) \Rightarrow a])) (AHead a1 a3) -(AHead a (asucc g a0)) H4) in ((let H7 \def (f_equal A A (\lambda (e: -A).(match e in A return (\lambda (_: A).A) with [(ASort _ _) \Rightarrow a1 | -(AHead a _) \Rightarrow a])) (AHead a1 a3) (AHead a (asucc g a0)) H4) in -(eq_ind A a (\lambda (a5: A).((eq A a3 (asucc g a0)) \to ((eq A (AHead a2 a4) -(ASort n1 n0)) \to ((leq g a5 a2) \to ((leq g a3 a4) \to (leq g (AHead a a0) -(ASort (S n1) n0))))))) (\lambda (H8: (eq A a3 (asucc g a0))).(eq_ind A -(asucc g a0) (\lambda (a5: A).((eq A (AHead a2 a4) (ASort n1 n0)) \to ((leq g -a a2) \to ((leq g a5 a4) \to (leq g (AHead a a0) (ASort (S n1) n0)))))) -(\lambda (H9: (eq A (AHead a2 a4) (ASort n1 n0))).(let H10 \def (eq_ind A -(AHead a2 a4) (\lambda (e: A).(match e in A return (\lambda (_: A).Prop) with -[(ASort _ _) \Rightarrow False | (AHead _ _) \Rightarrow True])) I (ASort n1 -n0) H9) in (False_ind ((leq g a a2) \to ((leq g (asucc g a0) a4) \to (leq g -(AHead a a0) (ASort (S n1) n0)))) H10))) a3 (sym_eq A a3 (asucc g a0) H8))) -a1 (sym_eq A a1 a H7))) H6)) H5 H2 H3)))]) in (H3 (refl_equal A (AHead a -(asucc g a0))) (refl_equal A (ASort n1 n0)))))]) H1)))) (\lambda (a3: -A).(\lambda (_: (((leq g (asucc g (AHead a a0)) (asucc g a3)) \to (leq g -(AHead a a0) a3)))).(\lambda (a4: A).(\lambda (_: (((leq g (asucc g (AHead a -a0)) (asucc g a4)) \to (leq g (AHead a a0) a4)))).(\lambda (H3: (leq g (asucc -g (AHead a a0)) (asucc g (AHead a3 a4)))).(let H4 \def (match H3 in leq -return (\lambda (a1: A).(\lambda (a2: A).(\lambda (_: (leq ? a1 a2)).((eq A -a1 (AHead a (asucc g a0))) \to ((eq A a2 (AHead a3 (asucc g a4))) \to (leq g -(AHead a a0) (AHead a3 a4))))))) with [(leq_sort h1 h2 n1 n2 k H4) -\Rightarrow (\lambda (H5: (eq A (ASort h1 n1) (AHead a (asucc g -a0)))).(\lambda (H6: (eq A (ASort h2 n2) (AHead a3 (asucc g a4)))).((let H7 -\def (eq_ind A (ASort h1 n1) (\lambda (e: A).(match e in A return (\lambda -(_: A).Prop) with [(ASort _ _) \Rightarrow True | (AHead _ _) \Rightarrow -False])) I (AHead a (asucc g a0)) H5) in (False_ind ((eq A (ASort h2 n2) -(AHead a3 (asucc g a4))) \to ((eq A (aplus g (ASort h1 n1) k) (aplus g (ASort -h2 n2) k)) \to (leq g (AHead a a0) (AHead a3 a4)))) H7)) H6 H4))) | (leq_head -a3 a4 H4 a5 a6 H5) \Rightarrow (\lambda (H6: (eq A (AHead a3 a5) (AHead a -(asucc g a0)))).(\lambda (H7: (eq A (AHead a4 a6) (AHead a3 (asucc g -a4)))).((let H8 \def (f_equal A A (\lambda (e: A).(match e in A return -(\lambda (_: A).A) with [(ASort _ _) \Rightarrow a5 | (AHead _ a) \Rightarrow -a])) (AHead a3 a5) (AHead a (asucc g a0)) H6) in ((let H9 \def (f_equal A A -(\lambda (e: A).(match e in A return (\lambda (_: A).A) with [(ASort _ _) -\Rightarrow a3 | (AHead a _) \Rightarrow a])) (AHead a3 a5) (AHead a (asucc g -a0)) H6) in (eq_ind A a (\lambda (a1: A).((eq A a5 (asucc g a0)) \to ((eq A -(AHead a4 a6) (AHead a3 (asucc g a4))) \to ((leq g a1 a4) \to ((leq g a5 a6) -\to (leq g (AHead a a0) (AHead a3 a4))))))) (\lambda (H10: (eq A a5 (asucc g -a0))).(eq_ind A (asucc g a0) (\lambda (a1: A).((eq A (AHead a4 a6) (AHead a3 -(asucc g a4))) \to ((leq g a a4) \to ((leq g a1 a6) \to (leq g (AHead a a0) -(AHead a3 a4)))))) (\lambda (H11: (eq A (AHead a4 a6) (AHead a3 (asucc g -a4)))).(let H12 \def (f_equal A A (\lambda (e: A).(match e in A return -(\lambda (_: A).A) with [(ASort _ _) \Rightarrow a6 | (AHead _ a) \Rightarrow -a])) (AHead a4 a6) (AHead a3 (asucc g a4)) H11) in ((let H13 \def (f_equal A -A (\lambda (e: A).(match e in A return (\lambda (_: A).A) with [(ASort _ _) -\Rightarrow a4 | (AHead a _) \Rightarrow a])) (AHead a4 a6) (AHead a3 (asucc -g a4)) H11) in (eq_ind A a3 (\lambda (a1: A).((eq A a6 (asucc g a4)) \to -((leq g a a1) \to ((leq g (asucc g a0) a6) \to (leq g (AHead a a0) (AHead a3 -a4)))))) (\lambda (H14: (eq A a6 (asucc g a4))).(eq_ind A (asucc g a4) -(\lambda (a1: A).((leq g a a3) \to ((leq g (asucc g a0) a1) \to (leq g (AHead -a a0) (AHead a3 a4))))) (\lambda (H15: (leq g a a3)).(\lambda (H16: (leq g -(asucc g a0) (asucc g a4))).(leq_head g a a3 H15 a0 a4 (H0 a4 H16)))) a6 -(sym_eq A a6 (asucc g a4) H14))) a4 (sym_eq A a4 a3 H13))) H12))) a5 (sym_eq -A a5 (asucc g a0) H10))) a3 (sym_eq A a3 a H9))) H8)) H7 H4 H5)))]) in (H4 -(refl_equal A (AHead a (asucc g a0))) (refl_equal A (AHead a3 (asucc g -a4)))))))))) a2)))))) a1)). - diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/problems.ma b/matita/contribs/LAMBDA-TYPES/Level-1/problems.ma index 9f9ce1b36..0e740a878 100644 --- a/matita/contribs/LAMBDA-TYPES/Level-1/problems.ma +++ b/matita/contribs/LAMBDA-TYPES/Level-1/problems.ma @@ -20,9 +20,7 @@ include "LambdaDelta/theory.ma". (* Problem 1: disambiguation errors with these objects *) -(* iso_trans (in problems-1) - * drop1_getl_trans (in problems-2) - * asucc_inj (in problems-3) +(* leq_trans (in problems-4) *) (* Problem 2: assertion failure raised by type checker on this object *)