From: Ferruccio Guidi Date: Wed, 25 Oct 2006 14:12:08 +0000 (+0000) Subject: some patches. still does not compile properly X-Git-Tag: 0.4.95@7852~847 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=b7a015aa6d4947c1a8e13ff0691702b3aaa40de6;p=helm.git some patches. still does not compile properly --- diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/csuba/arity.ma b/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/csuba/arity.ma index fe9436497..acd564afb 100644 --- a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/csuba/arity.ma +++ b/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/csuba/arity.ma @@ -103,83 +103,10 @@ g c2 t0 a1))))).(\lambda (a2: A).(\lambda (H2: (leq g a1 a2)).(\lambda (c2: C).(\lambda (H3: (csuba g c c2)).(arity_repl g c2 t0 a1 (H1 c2 H3) a2 H2)))))))))) c1 t a H))))). -theorem csuba_arity_rev: +axiom csuba_arity_rev: \forall (g: G).(\forall (c1: C).(\forall (t: T).(\forall (a: A).((arity g c1 t a) \to (\forall (c2: C).((csuba g c2 c1) \to (arity g c2 t a))))))) -\def - \lambda (g: G).(\lambda (c1: C).(\lambda (t: T).(\lambda (a: A).(\lambda (H: -(arity g c1 t a)).(arity_ind g (\lambda (c: C).(\lambda (t0: T).(\lambda (a0: -A).(\forall (c2: C).((csuba g c2 c) \to (arity g c2 t0 a0)))))) (\lambda (c: -C).(\lambda (n: nat).(\lambda (c2: C).(\lambda (_: (csuba g c2 -c)).(arity_sort g c2 n))))) (\lambda (c: C).(\lambda (d: C).(\lambda (u: -T).(\lambda (i: nat).(\lambda (H0: (getl i c (CHead d (Bind Abbr) -u))).(\lambda (a0: A).(\lambda (H1: (arity g d u a0)).(\lambda (H2: ((\forall -(c2: C).((csuba g c2 d) \to (arity g c2 u a0))))).(\lambda (c2: C).(\lambda -(H3: (csuba g c2 c)).(let H4 \def (csuba_getl_abbr_rev g c d u i H0 c2 H3) in -(or_ind (ex2 C (\lambda (d2: C).(getl i c2 (CHead d2 (Bind Abbr) u))) -(\lambda (d2: C).(csuba g d2 d))) (ex4_3 C T A (\lambda (d2: C).(\lambda (u2: -T).(\lambda (_: A).(getl i c2 (CHead d2 (Bind Abst) u2))))) (\lambda (d2: -C).(\lambda (_: T).(\lambda (_: A).(csuba g d2 d)))) (\lambda (d2: -C).(\lambda (u2: T).(\lambda (a1: A).(arity g d2 u2 (asucc g a1))))) (\lambda -(_: C).(\lambda (_: T).(\lambda (a1: A).(arity g d u a1))))) (arity g c2 -(TLRef i) a0) (\lambda (H5: (ex2 C (\lambda (d2: C).(getl i c2 (CHead d2 -(Bind Abbr) u))) (\lambda (d2: C).(csuba g d2 d)))).(ex2_ind C (\lambda (d2: -C).(getl i c2 (CHead d2 (Bind Abbr) u))) (\lambda (d2: C).(csuba g d2 d)) -(arity g c2 (TLRef i) a0) (\lambda (x: C).(\lambda (H6: (getl i c2 (CHead x -(Bind Abbr) u))).(\lambda (H7: (csuba g x d)).(arity_abbr g c2 x u i H6 a0 -(H2 x H7))))) H5)) (\lambda (H5: (ex4_3 C T A (\lambda (d2: C).(\lambda (u2: -T).(\lambda (_: A).(getl i c2 (CHead d2 (Bind Abst) u2))))) (\lambda (d2: -C).(\lambda (_: T).(\lambda (_: A).(csuba g d2 d)))) (\lambda (d2: -C).(\lambda (u2: T).(\lambda (a1: A).(arity g d2 u2 (asucc g a1))))) (\lambda -(_: C).(\lambda (_: T).(\lambda (a1: A).(arity g d u a1)))))).(ex4_3_ind C T -A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(getl i c2 (CHead d2 -(Bind Abst) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g -d2 d)))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a1: A).(arity g d2 u2 -(asucc g a1))))) (\lambda (_: C).(\lambda (_: T).(\lambda (a1: A).(arity g d -u a1)))) (arity g c2 (TLRef i) a0) (\lambda (x0: C).(\lambda (x1: T).(\lambda -(x2: A).(\lambda (H6: (getl i c2 (CHead x0 (Bind Abst) x1))).(\lambda (_: -(csuba g x0 d)).(\lambda (H8: (arity g x0 x1 (asucc g x2))).(\lambda (H9: -(arity g d u x2)).(arity_repl g c2 (TLRef i) x2 (arity_abst g c2 x0 x1 i H6 -x2 H8) a0 (arity_mono g d u x2 H9 a0 H1))))))))) H5)) H4)))))))))))) (\lambda -(c: C).(\lambda (d: C).(\lambda (u: T).(\lambda (i: nat).(\lambda (H0: (getl -i c (CHead d (Bind Abst) u))).(\lambda (a0: A).(\lambda (_: (arity g d u -(asucc g a0))).(\lambda (H2: ((\forall (c2: C).((csuba g c2 d) \to (arity g -c2 u (asucc g a0)))))).(\lambda (c2: C).(\lambda (H3: (csuba g c2 c)).(let H4 -\def (csuba_getl_abst_rev g c d u i H0 c2 H3) in (ex2_ind C (\lambda (d2: -C).(getl i c2 (CHead d2 (Bind Abst) u))) (\lambda (d2: C).(csuba g d2 d)) -(arity g c2 (TLRef i) a0) (\lambda (x: C).(\lambda (H5: (getl i c2 (CHead x -(Bind Abst) u))).(\lambda (H6: (csuba g x d)).(arity_abst g c2 x u i H5 a0 -(H2 x H6))))) H4)))))))))))) (\lambda (b: B).(\lambda (H0: (not (eq B b -Abst))).(\lambda (c: C).(\lambda (u: T).(\lambda (a1: A).(\lambda (_: (arity -g c u a1)).(\lambda (H2: ((\forall (c2: C).((csuba g c2 c) \to (arity g c2 u -a1))))).(\lambda (t0: T).(\lambda (a2: A).(\lambda (_: (arity g (CHead c -(Bind b) u) t0 a2)).(\lambda (H4: ((\forall (c2: C).((csuba g c2 (CHead c -(Bind b) u)) \to (arity g c2 t0 a2))))).(\lambda (c2: C).(\lambda (H5: (csuba -g c2 c)).(arity_bind g b H0 c2 u a1 (H2 c2 H5) t0 a2 (H4 (CHead c2 (Bind b) -u) (csuba_head g c2 c H5 (Bind b) u)))))))))))))))) (\lambda (c: C).(\lambda -(u: T).(\lambda (a1: A).(\lambda (_: (arity g c u (asucc g a1))).(\lambda -(H1: ((\forall (c2: C).((csuba g c2 c) \to (arity g c2 u (asucc g -a1)))))).(\lambda (t0: T).(\lambda (a2: A).(\lambda (_: (arity g (CHead c -(Bind Abst) u) t0 a2)).(\lambda (H3: ((\forall (c2: C).((csuba g c2 (CHead c -(Bind Abst) u)) \to (arity g c2 t0 a2))))).(\lambda (c2: C).(\lambda (H4: -(csuba g c2 c)).(arity_head g c2 u a1 (H1 c2 H4) t0 a2 (H3 (CHead c2 (Bind -Abst) u) (csuba_head g c2 c H4 (Bind Abst) u)))))))))))))) (\lambda (c: -C).(\lambda (u: T).(\lambda (a1: A).(\lambda (_: (arity g c u a1)).(\lambda -(H1: ((\forall (c2: C).((csuba g c2 c) \to (arity g c2 u a1))))).(\lambda -(t0: T).(\lambda (a2: A).(\lambda (_: (arity g c t0 (AHead a1 a2))).(\lambda -(H3: ((\forall (c2: C).((csuba g c2 c) \to (arity g c2 t0 (AHead a1 -a2)))))).(\lambda (c2: C).(\lambda (H4: (csuba g c2 c)).(arity_appl g c2 u a1 -(H1 c2 H4) t0 a2 (H3 c2 H4))))))))))))) (\lambda (c: C).(\lambda (u: -T).(\lambda (a0: A).(\lambda (_: (arity g c u (asucc g a0))).(\lambda (H1: -((\forall (c2: C).((csuba g c2 c) \to (arity g c2 u (asucc g -a0)))))).(\lambda (t0: T).(\lambda (_: (arity g c t0 a0)).(\lambda (H3: -((\forall (c2: C).((csuba g c2 c) \to (arity g c2 t0 a0))))).(\lambda (c2: -C).(\lambda (H4: (csuba g c2 c)).(arity_cast g c2 u a0 (H1 c2 H4) t0 (H3 c2 -H4)))))))))))) (\lambda (c: C).(\lambda (t0: T).(\lambda (a1: A).(\lambda (_: -(arity g c t0 a1)).(\lambda (H1: ((\forall (c2: C).((csuba g c2 c) \to (arity -g c2 t0 a1))))).(\lambda (a2: A).(\lambda (H2: (leq g a1 a2)).(\lambda (c2: -C).(\lambda (H3: (csuba g c2 c)).(arity_repl g c2 t0 a1 (H1 c2 H3) a2 -H2)))))))))) c1 t a H))))). +. theorem arity_appls_appl: \forall (g: G).(\forall (c: C).(\forall (v: T).(\forall (a1: A).((arity g c diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/iso/fwd.ma b/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/iso/fwd.ma index 038a53cf8..9402e8cbf 100644 --- a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/iso/fwd.ma +++ b/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/iso/fwd.ma @@ -201,3 +201,111 @@ H9))) t3 (sym_eq T t3 (THeads (Flat f1) t1 (THead (Flat f2) v2 t2)) H7))) v1 (refl_equal T (THead (Flat f1) t0 (THeads (Flat f1) t1 (THead (Flat f2) v2 t2)))) (refl_equal T (THead (Bind b) v t))))))))) vs)))))))). +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))))))). + 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 2396280a3..539d32575 100644 --- a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/iso/props.ma +++ b/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/iso/props.ma @@ -16,7 +16,7 @@ set "baseuri" "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/iso/props". -include "iso/defs.ma". +include "iso/fwd.ma". theorem iso_trans: \forall (t1: T).(\forall (t2: T).((iso t1 t2) \to (\forall (t3: T).((iso t2 diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/subst0/dec.ma b/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/subst0/dec.ma index 8f59bf3ee..77c87f905 100644 --- a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/subst0/dec.ma +++ b/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/subst0/dec.ma @@ -20,6 +20,136 @@ include "subst0/defs.ma". include "lift/props.ma". +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 dnf_dec: \forall (w: T).(\forall (t: T).(\forall (d: nat).(ex T (\lambda (v: T).(or (subst0 d w t (lift (S O) d v)) (eq T t (lift (S O) d v)))))))