From 061e94c62f89915a193ebd342cefe4be1f8d2869 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Sun, 29 Oct 2006 15:11:56 +0000 Subject: [PATCH] Level-1/LambdaDelta now compiles fine --- .../LAMBDA-TYPES/Level-1/LambdaDelta.ma | 256 ------------------ .../Level-1/LambdaDelta/pr3/props.ma | 10 + 2 files changed, 10 insertions(+), 256 deletions(-) diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta.ma b/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta.ma index 7e15f1539..675dbfe7c 100644 --- a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta.ma +++ b/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta.ma @@ -146,122 +146,6 @@ t1)) (H0 x0 x1 (H2 x0 (eq_ind nat (tslen t0) (\lambda (n: nat).(lt n (tslen (TCons t t0)))) (le_n (tslen (TCons t t0))) (tslen x0) H5))) (TCons t t0) H4))))) H3))))))) ts2)) ts)))). -theorem iso_gen_sort: - \forall (u2: T).(\forall (n1: nat).((iso (TSort n1) u2) \to (ex nat (\lambda -(n2: nat).(eq T u2 (TSort n2)))))) -\def - \lambda (u2: T).(\lambda (n1: nat).(\lambda (H: (iso (TSort n1) u2)).(let H0 -\def (match H in iso return (\lambda (t: T).(\lambda (t0: T).(\lambda (_: -(iso t t0)).((eq T t (TSort n1)) \to ((eq T t0 u2) \to (ex nat (\lambda (n2: -nat).(eq T u2 (TSort n2))))))))) with [(iso_sort n0 n2) \Rightarrow (\lambda -(H0: (eq T (TSort n0) (TSort n1))).(\lambda (H1: (eq T (TSort n2) u2)).((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 n1) H0) in (eq_ind nat n1 (\lambda (_: -nat).((eq T (TSort n2) u2) \to (ex nat (\lambda (n3: nat).(eq T u2 (TSort -n3)))))) (\lambda (H3: (eq T (TSort n2) u2)).(eq_ind T (TSort n2) (\lambda -(t: T).(ex nat (\lambda (n3: nat).(eq T t (TSort n3))))) (ex_intro nat -(\lambda (n3: nat).(eq T (TSort n2) (TSort n3))) n2 (refl_equal T (TSort -n2))) u2 H3)) n0 (sym_eq nat n0 n1 H2))) H1))) | (iso_lref i1 i2) \Rightarrow -(\lambda (H0: (eq T (TLRef i1) (TSort n1))).(\lambda (H1: (eq T (TLRef i2) -u2)).((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 n1) H0) in -(False_ind ((eq T (TLRef i2) u2) \to (ex nat (\lambda (n2: nat).(eq T u2 -(TSort n2))))) H2)) H1))) | (iso_head v1 v2 t1 t2 k) \Rightarrow (\lambda -(H0: (eq T (THead k v1 t1) (TSort n1))).(\lambda (H1: (eq T (THead k v2 t2) -u2)).((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 n1) H0) in -(False_ind ((eq T (THead k v2 t2) u2) \to (ex nat (\lambda (n2: nat).(eq T u2 -(TSort n2))))) H2)) H1)))]) in (H0 (refl_equal T (TSort n1)) (refl_equal T -u2))))). - -theorem iso_gen_lref: - \forall (u2: T).(\forall (n1: nat).((iso (TLRef n1) u2) \to (ex nat (\lambda -(n2: nat).(eq T u2 (TLRef n2)))))) -\def - \lambda (u2: T).(\lambda (n1: nat).(\lambda (H: (iso (TLRef n1) u2)).(let H0 -\def (match H in iso return (\lambda (t: T).(\lambda (t0: T).(\lambda (_: -(iso t t0)).((eq T t (TLRef n1)) \to ((eq T t0 u2) \to (ex nat (\lambda (n2: -nat).(eq T u2 (TLRef n2))))))))) with [(iso_sort n0 n2) \Rightarrow (\lambda -(H0: (eq T (TSort n0) (TLRef n1))).(\lambda (H1: (eq T (TSort n2) u2)).((let -H2 \def (eq_ind T (TSort n0) (\lambda (e: T).(match e in T return (\lambda -(_: T).Prop) with [(TSort _) \Rightarrow True | (TLRef _) \Rightarrow False | -(THead _ _ _) \Rightarrow False])) I (TLRef n1) H0) in (False_ind ((eq T -(TSort n2) u2) \to (ex nat (\lambda (n3: nat).(eq T u2 (TLRef n3))))) H2)) -H1))) | (iso_lref i1 i2) \Rightarrow (\lambda (H0: (eq T (TLRef i1) (TLRef -n1))).(\lambda (H1: (eq T (TLRef i2) u2)).((let H2 \def (f_equal T nat -(\lambda (e: T).(match e in T return (\lambda (_: T).nat) with [(TSort _) -\Rightarrow i1 | (TLRef n) \Rightarrow n | (THead _ _ _) \Rightarrow i1])) -(TLRef i1) (TLRef n1) H0) in (eq_ind nat n1 (\lambda (_: nat).((eq T (TLRef -i2) u2) \to (ex nat (\lambda (n2: nat).(eq T u2 (TLRef n2)))))) (\lambda (H3: -(eq T (TLRef i2) u2)).(eq_ind T (TLRef i2) (\lambda (t: T).(ex nat (\lambda -(n2: nat).(eq T t (TLRef n2))))) (ex_intro nat (\lambda (n2: nat).(eq T -(TLRef i2) (TLRef n2))) i2 (refl_equal T (TLRef i2))) u2 H3)) i1 (sym_eq nat -i1 n1 H2))) H1))) | (iso_head v1 v2 t1 t2 k) \Rightarrow (\lambda (H0: (eq T -(THead k v1 t1) (TLRef n1))).(\lambda (H1: (eq T (THead k v2 t2) u2)).((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 n1) H0) in -(False_ind ((eq T (THead k v2 t2) u2) \to (ex nat (\lambda (n2: nat).(eq T u2 -(TLRef n2))))) H2)) H1)))]) in (H0 (refl_equal T (TLRef n1)) (refl_equal T -u2))))). - -theorem iso_gen_head: - \forall (k: K).(\forall (v1: T).(\forall (t1: T).(\forall (u2: T).((iso -(THead k v1 t1) u2) \to (ex_2 T T (\lambda (v2: T).(\lambda (t2: T).(eq T u2 -(THead k v2 t2))))))))) -\def - \lambda (k: K).(\lambda (v1: T).(\lambda (t1: T).(\lambda (u2: T).(\lambda -(H: (iso (THead k v1 t1) u2)).(let H0 \def (match H in iso return (\lambda -(t: T).(\lambda (t0: T).(\lambda (_: (iso t t0)).((eq T t (THead k v1 t1)) -\to ((eq T t0 u2) \to (ex_2 T T (\lambda (v2: T).(\lambda (t2: T).(eq T u2 -(THead k v2 t2)))))))))) with [(iso_sort n1 n2) \Rightarrow (\lambda (H0: (eq -T (TSort n1) (THead k v1 t1))).(\lambda (H1: (eq T (TSort n2) u2)).((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 v1 t1) H0) in (False_ind ((eq T -(TSort n2) u2) \to (ex_2 T T (\lambda (v2: T).(\lambda (t2: T).(eq T u2 -(THead k v2 t2)))))) H2)) H1))) | (iso_lref i1 i2) \Rightarrow (\lambda (H0: -(eq T (TLRef i1) (THead k v1 t1))).(\lambda (H1: (eq T (TLRef i2) u2)).((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 v1 t1) H0) in (False_ind ((eq T -(TLRef i2) u2) \to (ex_2 T T (\lambda (v2: T).(\lambda (t2: T).(eq T u2 -(THead k v2 t2)))))) H2)) H1))) | (iso_head v0 v2 t0 t2 k0) \Rightarrow -(\lambda (H0: (eq T (THead k0 v0 t0) (THead k v1 t1))).(\lambda (H1: (eq T -(THead k0 v2 t2) u2)).((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 v1 -t1) 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 v1 t1) 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 k1 _ -_) \Rightarrow k1])) (THead k0 v0 t0) (THead k v1 t1) H0) in (eq_ind K k -(\lambda (k1: K).((eq T v0 v1) \to ((eq T t0 t1) \to ((eq T (THead k1 v2 t2) -u2) \to (ex_2 T T (\lambda (v3: T).(\lambda (t3: T).(eq T u2 (THead k v3 -t3))))))))) (\lambda (H5: (eq T v0 v1)).(eq_ind T v1 (\lambda (_: T).((eq T -t0 t1) \to ((eq T (THead k v2 t2) u2) \to (ex_2 T T (\lambda (v3: T).(\lambda -(t3: T).(eq T u2 (THead k v3 t3)))))))) (\lambda (H6: (eq T t0 t1)).(eq_ind T -t1 (\lambda (_: T).((eq T (THead k v2 t2) u2) \to (ex_2 T T (\lambda (v3: -T).(\lambda (t3: T).(eq T u2 (THead k v3 t3))))))) (\lambda (H7: (eq T (THead -k v2 t2) u2)).(eq_ind T (THead k v2 t2) (\lambda (t: T).(ex_2 T T (\lambda -(v3: T).(\lambda (t3: T).(eq T t (THead k v3 t3)))))) (ex_2_intro T T -(\lambda (v3: T).(\lambda (t3: T).(eq T (THead k v2 t2) (THead k v3 t3)))) v2 -t2 (refl_equal T (THead k v2 t2))) u2 H7)) t0 (sym_eq T t0 t1 H6))) v0 -(sym_eq T v0 v1 H5))) k0 (sym_eq K k0 k H4))) H3)) H2)) H1)))]) in (H0 -(refl_equal T (THead k v1 t1)) (refl_equal T u2))))))). - -theorem iso_refl: - \forall (t: T).(iso t t) -\def - \lambda (t: T).(T_ind (\lambda (t0: T).(iso t0 t0)) (\lambda (n: -nat).(iso_sort n n)) (\lambda (n: nat).(iso_lref n n)) (\lambda (k: -K).(\lambda (t0: T).(\lambda (_: (iso t0 t0)).(\lambda (t1: T).(\lambda (_: -(iso t1 t1)).(iso_head t0 t0 t1 t1 k)))))) t). - theorem lifts_tapp: \forall (h: nat).(\forall (d: nat).(\forall (v: T).(\forall (vs: TList).(eq TList (lifts h d (TApp vs v)) (TApp (lifts h d vs) (lift h d v)))))) @@ -276,136 +160,6 @@ t0) (lift h d v)) (\lambda (t1: TList).(eq TList (TCons (lift h d t) t1) (TCons (lift h d t) (TApp (lifts h d t0) (lift h d v)))) (lifts h d (TApp t0 v)) H)))) vs)))). -theorem dnf_dec2: - \forall (t: T).(\forall (d: nat).(or (\forall (w: T).(ex T (\lambda (v: -T).(subst0 d w t (lift (S O) d v))))) (ex T (\lambda (v: T).(eq T t (lift (S -O) d v)))))) -\def - \lambda (t: T).(T_ind (\lambda (t0: T).(\forall (d: nat).(or (\forall (w: -T).(ex T (\lambda (v: T).(subst0 d w t0 (lift (S O) d v))))) (ex T (\lambda -(v: T).(eq T t0 (lift (S O) d v))))))) (\lambda (n: nat).(\lambda (d: -nat).(or_intror (\forall (w: T).(ex T (\lambda (v: T).(subst0 d w (TSort n) -(lift (S O) d v))))) (ex T (\lambda (v: T).(eq T (TSort n) (lift (S O) d -v)))) (ex_intro T (\lambda (v: T).(eq T (TSort n) (lift (S O) d v))) (TSort -n) (eq_ind_r T (TSort n) (\lambda (t0: T).(eq T (TSort n) t0)) (refl_equal T -(TSort n)) (lift (S O) d (TSort n)) (lift_sort n (S O) d)))))) (\lambda (n: -nat).(\lambda (d: nat).(lt_eq_gt_e n d (or (\forall (w: T).(ex T (\lambda (v: -T).(subst0 d w (TLRef n) (lift (S O) d v))))) (ex T (\lambda (v: T).(eq T -(TLRef n) (lift (S O) d v))))) (\lambda (H: (lt n d)).(or_intror (\forall (w: -T).(ex T (\lambda (v: T).(subst0 d w (TLRef n) (lift (S O) d v))))) (ex T -(\lambda (v: T).(eq T (TLRef n) (lift (S O) d v)))) (ex_intro T (\lambda (v: -T).(eq T (TLRef n) (lift (S O) d v))) (TLRef n) (eq_ind_r T (TLRef n) -(\lambda (t0: T).(eq T (TLRef n) t0)) (refl_equal T (TLRef n)) (lift (S O) d -(TLRef n)) (lift_lref_lt n (S O) d H))))) (\lambda (H: (eq nat n d)).(eq_ind -nat n (\lambda (n0: nat).(or (\forall (w: T).(ex T (\lambda (v: T).(subst0 n0 -w (TLRef n) (lift (S O) n0 v))))) (ex T (\lambda (v: T).(eq T (TLRef n) (lift -(S O) n0 v)))))) (or_introl (\forall (w: T).(ex T (\lambda (v: T).(subst0 n w -(TLRef n) (lift (S O) n v))))) (ex T (\lambda (v: T).(eq T (TLRef n) (lift (S -O) n v)))) (\lambda (w: T).(ex_intro T (\lambda (v: T).(subst0 n w (TLRef n) -(lift (S O) n v))) (lift n O w) (eq_ind_r T (lift (plus (S O) n) O w) -(\lambda (t0: T).(subst0 n w (TLRef n) t0)) (subst0_lref w n) (lift (S O) n -(lift n O w)) (lift_free w n (S O) O n (le_n (plus O n)) (le_O_n n)))))) d -H)) (\lambda (H: (lt d n)).(or_intror (\forall (w: T).(ex T (\lambda (v: -T).(subst0 d w (TLRef n) (lift (S O) d v))))) (ex T (\lambda (v: T).(eq T -(TLRef n) (lift (S O) d v)))) (ex_intro T (\lambda (v: T).(eq T (TLRef n) -(lift (S O) d v))) (TLRef (pred n)) (eq_ind_r T (TLRef n) (\lambda (t0: -T).(eq T (TLRef n) t0)) (refl_equal T (TLRef n)) (lift (S O) d (TLRef (pred -n))) (lift_lref_gt d n H)))))))) (\lambda (k: K).(\lambda (t0: T).(\lambda -(H: ((\forall (d: nat).(or (\forall (w: T).(ex T (\lambda (v: T).(subst0 d w -t0 (lift (S O) d v))))) (ex T (\lambda (v: T).(eq T t0 (lift (S O) d -v)))))))).(\lambda (t1: T).(\lambda (H0: ((\forall (d: nat).(or (\forall (w: -T).(ex T (\lambda (v: T).(subst0 d w t1 (lift (S O) d v))))) (ex T (\lambda -(v: T).(eq T t1 (lift (S O) d v)))))))).(\lambda (d: nat).(let H_x \def (H d) -in (let H1 \def H_x in (or_ind (\forall (w: T).(ex T (\lambda (v: T).(subst0 -d w t0 (lift (S O) d v))))) (ex T (\lambda (v: T).(eq T t0 (lift (S O) d -v)))) (or (\forall (w: T).(ex T (\lambda (v: T).(subst0 d w (THead k t0 t1) -(lift (S O) d v))))) (ex T (\lambda (v: T).(eq T (THead k t0 t1) (lift (S O) -d v))))) (\lambda (H2: ((\forall (w: T).(ex T (\lambda (v: T).(subst0 d w t0 -(lift (S O) d v))))))).(let H_x0 \def (H0 (s k d)) in (let H3 \def H_x0 in -(or_ind (\forall (w: T).(ex T (\lambda (v: T).(subst0 (s k d) w t1 (lift (S -O) (s k d) v))))) (ex T (\lambda (v: T).(eq T t1 (lift (S O) (s k d) v)))) -(or (\forall (w: T).(ex T (\lambda (v: T).(subst0 d w (THead k t0 t1) (lift -(S O) d v))))) (ex T (\lambda (v: T).(eq T (THead k t0 t1) (lift (S O) d -v))))) (\lambda (H4: ((\forall (w: T).(ex T (\lambda (v: T).(subst0 (s k d) w -t1 (lift (S O) (s k d) v))))))).(or_introl (\forall (w: T).(ex T (\lambda (v: -T).(subst0 d w (THead k t0 t1) (lift (S O) d v))))) (ex T (\lambda (v: T).(eq -T (THead k t0 t1) (lift (S O) d v)))) (\lambda (w: T).(let H_x1 \def (H4 w) -in (let H5 \def H_x1 in (ex_ind T (\lambda (v: T).(subst0 (s k d) w t1 (lift -(S O) (s k d) v))) (ex T (\lambda (v: T).(subst0 d w (THead k t0 t1) (lift (S -O) d v)))) (\lambda (x: T).(\lambda (H6: (subst0 (s k d) w t1 (lift (S O) (s -k d) x))).(let H_x2 \def (H2 w) in (let H7 \def H_x2 in (ex_ind T (\lambda -(v: T).(subst0 d w t0 (lift (S O) d v))) (ex T (\lambda (v: T).(subst0 d w -(THead k t0 t1) (lift (S O) d v)))) (\lambda (x0: T).(\lambda (H8: (subst0 d -w t0 (lift (S O) d x0))).(ex_intro T (\lambda (v: T).(subst0 d w (THead k t0 -t1) (lift (S O) d v))) (THead k x0 x) (eq_ind_r T (THead k (lift (S O) d x0) -(lift (S O) (s k d) x)) (\lambda (t2: T).(subst0 d w (THead k t0 t1) t2)) -(subst0_both w t0 (lift (S O) d x0) d H8 k t1 (lift (S O) (s k d) x) H6) -(lift (S O) d (THead k x0 x)) (lift_head k x0 x (S O) d))))) H7))))) H5)))))) -(\lambda (H4: (ex T (\lambda (v: T).(eq T t1 (lift (S O) (s k d) -v))))).(ex_ind T (\lambda (v: T).(eq T t1 (lift (S O) (s k d) v))) (or -(\forall (w: T).(ex T (\lambda (v: T).(subst0 d w (THead k t0 t1) (lift (S O) -d v))))) (ex T (\lambda (v: T).(eq T (THead k t0 t1) (lift (S O) d v))))) -(\lambda (x: T).(\lambda (H5: (eq T t1 (lift (S O) (s k d) x))).(eq_ind_r T -(lift (S O) (s k d) x) (\lambda (t2: T).(or (\forall (w: T).(ex T (\lambda -(v: T).(subst0 d w (THead k t0 t2) (lift (S O) d v))))) (ex T (\lambda (v: -T).(eq T (THead k t0 t2) (lift (S O) d v)))))) (or_introl (\forall (w: T).(ex -T (\lambda (v: T).(subst0 d w (THead k t0 (lift (S O) (s k d) x)) (lift (S O) -d v))))) (ex T (\lambda (v: T).(eq T (THead k t0 (lift (S O) (s k d) x)) -(lift (S O) d v)))) (\lambda (w: T).(let H_x1 \def (H2 w) in (let H6 \def -H_x1 in (ex_ind T (\lambda (v: T).(subst0 d w t0 (lift (S O) d v))) (ex T -(\lambda (v: T).(subst0 d w (THead k t0 (lift (S O) (s k d) x)) (lift (S O) d -v)))) (\lambda (x0: T).(\lambda (H7: (subst0 d w t0 (lift (S O) d -x0))).(ex_intro T (\lambda (v: T).(subst0 d w (THead k t0 (lift (S O) (s k d) -x)) (lift (S O) d v))) (THead k x0 x) (eq_ind_r T (THead k (lift (S O) d x0) -(lift (S O) (s k d) x)) (\lambda (t2: T).(subst0 d w (THead k t0 (lift (S O) -(s k d) x)) t2)) (subst0_fst w (lift (S O) d x0) t0 d H7 (lift (S O) (s k d) -x) k) (lift (S O) d (THead k x0 x)) (lift_head k x0 x (S O) d))))) H6))))) t1 -H5))) H4)) H3)))) (\lambda (H2: (ex T (\lambda (v: T).(eq T t0 (lift (S O) d -v))))).(ex_ind T (\lambda (v: T).(eq T t0 (lift (S O) d v))) (or (\forall (w: -T).(ex T (\lambda (v: T).(subst0 d w (THead k t0 t1) (lift (S O) d v))))) (ex -T (\lambda (v: T).(eq T (THead k t0 t1) (lift (S O) d v))))) (\lambda (x: -T).(\lambda (H3: (eq T t0 (lift (S O) d x))).(let H_x0 \def (H0 (s k d)) in -(let H4 \def H_x0 in (or_ind (\forall (w: T).(ex T (\lambda (v: T).(subst0 (s -k d) w t1 (lift (S O) (s k d) v))))) (ex T (\lambda (v: T).(eq T t1 (lift (S -O) (s k d) v)))) (or (\forall (w: T).(ex T (\lambda (v: T).(subst0 d w (THead -k t0 t1) (lift (S O) d v))))) (ex T (\lambda (v: T).(eq T (THead k t0 t1) -(lift (S O) d v))))) (\lambda (H5: ((\forall (w: T).(ex T (\lambda (v: -T).(subst0 (s k d) w t1 (lift (S O) (s k d) v))))))).(eq_ind_r T (lift (S O) -d x) (\lambda (t2: T).(or (\forall (w: T).(ex T (\lambda (v: T).(subst0 d w -(THead k t2 t1) (lift (S O) d v))))) (ex T (\lambda (v: T).(eq T (THead k t2 -t1) (lift (S O) d v)))))) (or_introl (\forall (w: T).(ex T (\lambda (v: -T).(subst0 d w (THead k (lift (S O) d x) t1) (lift (S O) d v))))) (ex T -(\lambda (v: T).(eq T (THead k (lift (S O) d x) t1) (lift (S O) d v)))) -(\lambda (w: T).(let H_x1 \def (H5 w) in (let H6 \def H_x1 in (ex_ind T -(\lambda (v: T).(subst0 (s k d) w t1 (lift (S O) (s k d) v))) (ex T (\lambda -(v: T).(subst0 d w (THead k (lift (S O) d x) t1) (lift (S O) d v)))) (\lambda -(x0: T).(\lambda (H7: (subst0 (s k d) w t1 (lift (S O) (s k d) -x0))).(ex_intro T (\lambda (v: T).(subst0 d w (THead k (lift (S O) d x) t1) -(lift (S O) d v))) (THead k x x0) (eq_ind_r T (THead k (lift (S O) d x) (lift -(S O) (s k d) x0)) (\lambda (t2: T).(subst0 d w (THead k (lift (S O) d x) t1) -t2)) (subst0_snd k w (lift (S O) (s k d) x0) t1 d H7 (lift (S O) d x)) (lift -(S O) d (THead k x x0)) (lift_head k x x0 (S O) d))))) H6))))) t0 H3)) -(\lambda (H5: (ex T (\lambda (v: T).(eq T t1 (lift (S O) (s k d) -v))))).(ex_ind T (\lambda (v: T).(eq T t1 (lift (S O) (s k d) v))) (or -(\forall (w: T).(ex T (\lambda (v: T).(subst0 d w (THead k t0 t1) (lift (S O) -d v))))) (ex T (\lambda (v: T).(eq T (THead k t0 t1) (lift (S O) d v))))) -(\lambda (x0: T).(\lambda (H6: (eq T t1 (lift (S O) (s k d) x0))).(eq_ind_r T -(lift (S O) (s k d) x0) (\lambda (t2: T).(or (\forall (w: T).(ex T (\lambda -(v: T).(subst0 d w (THead k t0 t2) (lift (S O) d v))))) (ex T (\lambda (v: -T).(eq T (THead k t0 t2) (lift (S O) d v)))))) (eq_ind_r T (lift (S O) d x) -(\lambda (t2: T).(or (\forall (w: T).(ex T (\lambda (v: T).(subst0 d w (THead -k t2 (lift (S O) (s k d) x0)) (lift (S O) d v))))) (ex T (\lambda (v: T).(eq -T (THead k t2 (lift (S O) (s k d) x0)) (lift (S O) d v)))))) (or_intror -(\forall (w: T).(ex T (\lambda (v: T).(subst0 d w (THead k (lift (S O) d x) -(lift (S O) (s k d) x0)) (lift (S O) d v))))) (ex T (\lambda (v: T).(eq T -(THead k (lift (S O) d x) (lift (S O) (s k d) x0)) (lift (S O) d v)))) -(ex_intro T (\lambda (v: T).(eq T (THead k (lift (S O) d x) (lift (S O) (s k -d) x0)) (lift (S O) d v))) (THead k x x0) (eq_ind_r T (THead k (lift (S O) d -x) (lift (S O) (s k d) x0)) (\lambda (t2: T).(eq T (THead k (lift (S O) d x) -(lift (S O) (s k d) x0)) t2)) (refl_equal T (THead k (lift (S O) d x) (lift -(S O) (s k d) x0))) (lift (S O) d (THead k x x0)) (lift_head k x x0 (S O) -d)))) t0 H3) t1 H6))) H5)) H4))))) H2)) H1))))))))) t). - theorem pr2_change: \forall (b: B).((not (eq B b Abbr)) \to (\forall (c: C).(\forall (v1: T).(\forall (t1: T).(\forall (t2: T).((pr2 (CHead c (Bind b) v1) t1 t2) \to @@ -456,16 +210,6 @@ u)) \to ((subst0 i0 u t4 t) \to (pr2 (CHead c (Bind b) v2) t3 t))))).(\lambda (CHead d (Bind Abbr) u) v1 i0 H7) v2) t3 t4 H3 t H8))))) i H6 H4))))))))))))) y t1 t2 H1))) H0)))))))). -theorem pr3_flat: - \forall (c: C).(\forall (u1: T).(\forall (u2: T).((pr3 c u1 u2) \to (\forall -(t1: T).(\forall (t2: T).((pr3 c t1 t2) \to (\forall (f: F).(pr3 c (THead -(Flat f) u1 t1) (THead (Flat f) u2 t2))))))))) -\def - \lambda (c: C).(\lambda (u1: T).(\lambda (u2: T).(\lambda (H: (pr3 c u1 -u2)).(\lambda (t1: T).(\lambda (t2: T).(\lambda (H0: (pr3 c t1 t2)).(\lambda -(f: F).(pr3_head_12 c u1 u2 H (Flat f) t1 t2 (pr3_cflat c t1 t2 H0 f -u2))))))))). - theorem pr3_gen_bind: \forall (b: B).((not (eq B b Abst)) \to (\forall (c: C).(\forall (u1: T).(\forall (t1: T).(\forall (x: T).((pr3 c (THead (Bind b) u1 t1) x) \to (or diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/pr3/props.ma b/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/pr3/props.ma index d77030f52..6916d8d40 100644 --- a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/pr3/props.ma +++ b/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/pr3/props.ma @@ -125,6 +125,16 @@ T).(\lambda (t4: T).(\lambda (H0: (pr2 c t4 t3)).(\lambda (t5: T).(\lambda c (Flat f) v) t3 t5))))).(\lambda (f: F).(\lambda (v: T).(pr3_sing (CHead c (Flat f) v) t3 t4 (pr2_cflat c t4 t3 H0 f v) t5 (H2 f v)))))))))) t1 t2 H)))). +theorem pr3_flat: + \forall (c: C).(\forall (u1: T).(\forall (u2: T).((pr3 c u1 u2) \to (\forall +(t1: T).(\forall (t2: T).((pr3 c t1 t2) \to (\forall (f: F).(pr3 c (THead +(Flat f) u1 t1) (THead (Flat f) u2 t2))))))))) +\def + \lambda (c: C).(\lambda (u1: T).(\lambda (u2: T).(\lambda (H: (pr3 c u1 +u2)).(\lambda (t1: T).(\lambda (t2: T).(\lambda (H0: (pr3 c t1 t2)).(\lambda +(f: F).(pr3_head_12 c u1 u2 H (Flat f) t1 t2 (pr3_cflat c t1 t2 H0 f +u2))))))))). + theorem pr3_pr0_pr2_t: \forall (u1: T).(\forall (u2: T).((pr0 u1 u2) \to (\forall (c: C).(\forall (t1: T).(\forall (t2: T).(\forall (k: K).((pr2 (CHead c k u2) t1 t2) \to (pr3 -- 2.39.2