From d6ce6da7d0d5572d7551adafe849f18ab8e8f895 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Tue, 11 Sep 2007 16:50:12 +0000 Subject: [PATCH] librarySync - we do not generate the object attributes when we publish the xml LambdaDelta-1 - new cast type rule --- components/cic_acic/cic2Xml.ml | 15 +- components/cic_acic/cic2Xml.mli | 1 + components/library/librarySync.ml | 9 +- .../LAMBDA-TYPES/LambdaDelta-1/ty3/arity.ma | 20 +- .../LAMBDA-TYPES/LambdaDelta-1/ty3/dec.ma | 54 ++-- .../LAMBDA-TYPES/LambdaDelta-1/ty3/defs.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/ty3/fsubst0.ma | 199 ++++++++------ .../LAMBDA-TYPES/LambdaDelta-1/ty3/fwd.ma | 242 ++++++++++-------- .../LAMBDA-TYPES/LambdaDelta-1/ty3/pr3.ma | 166 ++++++------ .../LambdaDelta-1/ty3/pr3_props.ma | 65 ++--- .../LAMBDA-TYPES/LambdaDelta-1/ty3/props.ma | 41 ++- .../LAMBDA-TYPES/LambdaDelta-1/ty3/subst1.ma | 140 +++++----- .../LAMBDA-TYPES/LambdaDelta-1/ty3/tau0.ma | 18 +- 13 files changed, 556 insertions(+), 416 deletions(-) diff --git a/components/cic_acic/cic2Xml.ml b/components/cic_acic/cic2Xml.ml index c90bc348c..eb3b93408 100644 --- a/components/cic_acic/cic2Xml.ml +++ b/components/cic_acic/cic2Xml.ml @@ -267,7 +267,7 @@ let print_term ?ids_to_inner_sorts = aux ;; -let xml_of_attrs attributes = +let xml_of_attrs generate_attributes attributes = let class_of = function | `Coercion n -> Xml.xml_empty "class" [None,"value","coercion";None,"arity",string_of_int n] @@ -312,9 +312,10 @@ let xml_of_attrs attributes = List.fold_right (fun attr res -> [< xml_attr_of attr ; res >]) attributes [<>] in - Xml.xml_nempty "attributes" [] xml_attrs + if generate_attributes then Xml.xml_nempty "attributes" [] xml_attrs else [<>] -let print_object uri ?ids_to_inner_sorts ~ask_dtd_to_the_getter obj = +let print_object uri + ?ids_to_inner_sorts ?(generate_attributes=true) ~ask_dtd_to_the_getter obj = let module C = Cic in let module X = Xml in let module U = UriManager in @@ -322,7 +323,7 @@ let print_object uri ?ids_to_inner_sorts ~ask_dtd_to_the_getter obj = match obj with C.ACurrentProof (id,idbody,n,conjectures,bo,ty,params,obj_attrs) -> let params' = param_attribute_of_params params in - let xml_attrs = xml_of_attrs obj_attrs in + let xml_attrs = xml_of_attrs generate_attributes obj_attrs in let xml_for_current_proof_body = (*CSC: Should the CurrentProof also have the list of variables it depends on? *) (*CSC: I think so. Not implemented yet. *) @@ -382,7 +383,7 @@ let print_object uri ?ids_to_inner_sorts ~ask_dtd_to_the_getter obj = xmlty, Some xmlbo | C.AConstant (id,idbody,n,bo,ty,params,obj_attrs) -> let params' = param_attribute_of_params params in - let xml_attrs = xml_of_attrs obj_attrs in + let xml_attrs = xml_of_attrs generate_attributes obj_attrs in let xmlbo = match bo with None -> None @@ -409,7 +410,7 @@ let print_object uri ?ids_to_inner_sorts ~ask_dtd_to_the_getter obj = xmlty, xmlbo | C.AVariable (id,n,bo,ty,params,obj_attrs) -> let params' = param_attribute_of_params params in - let xml_attrs = xml_of_attrs obj_attrs in + let xml_attrs = xml_of_attrs generate_attributes obj_attrs in let xmlbo = match bo with None -> [< >] @@ -429,7 +430,7 @@ let print_object uri ?ids_to_inner_sorts ~ask_dtd_to_the_getter obj = aobj, None | C.AInductiveDefinition (id,tys,params,nparams,obj_attrs) -> let params' = param_attribute_of_params params in - let xml_attrs = xml_of_attrs obj_attrs in + let xml_attrs = xml_of_attrs generate_attributes obj_attrs in [< X.xml_cdata "\n" ; X.xml_cdata ("\n") ; diff --git a/components/cic_acic/cic2Xml.mli b/components/cic_acic/cic2Xml.mli index 22c5669df..dcbff3d0f 100644 --- a/components/cic_acic/cic2Xml.mli +++ b/components/cic_acic/cic2Xml.mli @@ -33,6 +33,7 @@ val print_term : val print_object : UriManager.uri -> ?ids_to_inner_sorts: (string, Cic2acic.sort_kind) Hashtbl.t -> + ?generate_attributes:bool -> ask_dtd_to_the_getter:bool -> Cic.annobj -> Xml.token Stream.t * Xml.token Stream.t option diff --git a/components/library/librarySync.ml b/components/library/librarySync.ml index 11dccaaa1..9b08ba6dc 100644 --- a/components/library/librarySync.ml +++ b/components/library/librarySync.ml @@ -70,7 +70,7 @@ let save_object_to_disk uri obj ugraph univlist = HExtlib.mkdir dir in (* generate annobj, ids_to_inner_sorts and ids_to_inner_types *) - let annobj, innertypes, ids_to_inner_sorts = + let annobj, innertypes, ids_to_inner_sorts, generate_attributes = if Helm_registry.get_bool "matita.system" then let annobj, _, _, ids_to_inner_sorts, ids_to_inner_types, _, _ = Cic2acic.acic_object_of_cic_object obj @@ -79,15 +79,16 @@ let save_object_to_disk uri obj ugraph univlist = Cic2Xml.print_inner_types uri ~ids_to_inner_sorts ~ids_to_inner_types ~ask_dtd_to_the_getter:false in - annobj, Some innertypesxml, Some ids_to_inner_sorts + annobj, Some innertypesxml, Some ids_to_inner_sorts, false else let annobj = Cic2acic.plain_acic_object_of_cic_object obj in - annobj, None, None + annobj, None, None, true in (* prepare XML *) let xml, bodyxml = Cic2Xml.print_object - uri ?ids_to_inner_sorts ~ask_dtd_to_the_getter:false annobj + uri ?ids_to_inner_sorts ~ask_dtd_to_the_getter:false + ~generate_attributes annobj in let xmlpath, xmlbodypath, innertypespath, bodyuri, innertypesuri, xmlunivgraphpath, univgraphuri = diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/arity.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/arity.ma index 25d4ad924..ba58219da 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/arity.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/arity.ma @@ -178,13 +178,21 @@ g x3) (arity_head g c0 u x H6 t (asucc g x3) H18)))))))) H15)))))))) H10))))) H7))))) H4))))))))))) (\lambda (c0: C).(\lambda (t3: T).(\lambda (t4: T).(\lambda (_: (ty3 g c0 t3 t4)).(\lambda (H1: (ex2 A (\lambda (a1: A).(arity g c0 t3 a1)) (\lambda (a1: A).(arity g c0 t4 (asucc g -a1))))).(\lambda (t0: T).(\lambda (_: (ty3 g c0 t4 t0)).(\lambda (_: (ex2 A +a1))))).(\lambda (t0: T).(\lambda (_: (ty3 g c0 t4 t0)).(\lambda (H3: (ex2 A (\lambda (a1: A).(arity g c0 t4 a1)) (\lambda (a1: A).(arity g c0 t0 (asucc g a1))))).(let H4 \def H1 in (ex2_ind A (\lambda (a1: A).(arity g c0 t3 a1)) (\lambda (a1: A).(arity g c0 t4 (asucc g a1))) (ex2 A (\lambda (a1: A).(arity -g c0 (THead (Flat Cast) t4 t3) a1)) (\lambda (a1: A).(arity g c0 t4 (asucc g -a1)))) (\lambda (x: A).(\lambda (H5: (arity g c0 t3 x)).(\lambda (H6: (arity -g c0 t4 (asucc g x))).(ex_intro2 A (\lambda (a1: A).(arity g c0 (THead (Flat -Cast) t4 t3) a1)) (\lambda (a1: A).(arity g c0 t4 (asucc g a1))) x -(arity_cast g c0 t4 x H6 t3 H5) H6)))) H4)))))))))) c t1 t2 H))))). +g c0 (THead (Flat Cast) t4 t3) a1)) (\lambda (a1: A).(arity g c0 (THead (Flat +Cast) t0 t4) (asucc g a1)))) (\lambda (x: A).(\lambda (H5: (arity g c0 t3 +x)).(\lambda (H6: (arity g c0 t4 (asucc g x))).(let H7 \def H3 in (ex2_ind A +(\lambda (a1: A).(arity g c0 t4 a1)) (\lambda (a1: A).(arity g c0 t0 (asucc g +a1))) (ex2 A (\lambda (a1: A).(arity g c0 (THead (Flat Cast) t4 t3) a1)) +(\lambda (a1: A).(arity g c0 (THead (Flat Cast) t0 t4) (asucc g a1)))) +(\lambda (x0: A).(\lambda (H8: (arity g c0 t4 x0)).(\lambda (H9: (arity g c0 +t0 (asucc g x0))).(ex_intro2 A (\lambda (a1: A).(arity g c0 (THead (Flat +Cast) t4 t3) a1)) (\lambda (a1: A).(arity g c0 (THead (Flat Cast) t0 t4) +(asucc g a1))) x (arity_cast g c0 t4 x H6 t3 H5) (arity_cast g c0 t0 (asucc g +x) (arity_repl g c0 t0 (asucc g x0) H9 (asucc g (asucc g x)) (asucc_repl g x0 +(asucc g x) (arity_mono g c0 t4 x0 H8 (asucc g x) H6))) t4 H6))))) H7))))) +H4)))))))))) c t1 t2 H))))). diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/dec.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/dec.ma index 4a8ed6c73..ff4a0734e 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/dec.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/dec.ma @@ -435,28 +435,36 @@ Cast) t t0) t3) \to (\forall (P: Prop).P)))) (\lambda (H12: (pc3 c2 x0 t)).(or_introl (ex T (\lambda (t3: T).(ty3 g c2 (THead (Flat Cast) t t0) t3))) (\forall (t3: T).((ty3 g c2 (THead (Flat Cast) t t0) t3) \to (\forall (P: Prop).P))) (ex_intro T (\lambda (t3: T).(ty3 g c2 (THead (Flat Cast) t -t0) t3)) t (ty3_cast g c2 t0 t (ty3_conv g c2 t x H6 t0 x0 H9 H12) x H6)))) -(\lambda (H12: (((pc3 c2 x0 t) \to (\forall (P: Prop).P)))).(or_intror (ex T -(\lambda (t3: T).(ty3 g c2 (THead (Flat Cast) t t0) t3))) (\forall (t3: -T).((ty3 g c2 (THead (Flat Cast) t t0) t3) \to (\forall (P: Prop).P))) -(\lambda (t3: T).(\lambda (H13: (ty3 g c2 (THead (Flat Cast) t t0) -t3)).(\lambda (P: Prop).(and_ind (pc3 c2 t t3) (ty3 g c2 t0 t) P (\lambda (_: -(pc3 c2 t t3)).(\lambda (H15: (ty3 g c2 t0 t)).(let H_y \def (ty3_unique g c2 -t0 t H15 x0 H9) in (H12 (pc3_s c2 x0 t H_y) P)))) (ty3_gen_cast g c2 t0 t t3 -H13))))))) H11))))) (ty3_correct g c2 t0 x0 H9)))) H8)) (\lambda (H8: -((\forall (t3: T).((ty3 g c2 t0 t3) \to (\forall (P: Prop).P))))).(or_intror -(ex T (\lambda (t3: T).(ty3 g c2 (THead (Flat Cast) t t0) t3))) (\forall (t3: -T).((ty3 g c2 (THead (Flat Cast) t t0) t3) \to (\forall (P: Prop).P))) -(\lambda (t3: T).(\lambda (H9: (ty3 g c2 (THead (Flat Cast) t t0) -t3)).(\lambda (P: Prop).(and_ind (pc3 c2 t t3) (ty3 g c2 t0 t) P (\lambda (_: -(pc3 c2 t t3)).(\lambda (H11: (ty3 g c2 t0 t)).(H8 t H11 P))) (ty3_gen_cast g -c2 t0 t t3 H9))))))) H7)))) H5)) (\lambda (H5: ((\forall (t3: T).((ty3 g c2 t -t3) \to (\forall (P: Prop).P))))).(or_intror (ex T (\lambda (t3: T).(ty3 g c2 -(THead (Flat Cast) t t0) t3))) (\forall (t3: T).((ty3 g c2 (THead (Flat Cast) -t t0) t3) \to (\forall (P: Prop).P))) (\lambda (t3: T).(\lambda (H6: (ty3 g -c2 (THead (Flat Cast) t t0) t3)).(\lambda (P: Prop).(and_ind (pc3 c2 t t3) -(ty3 g c2 t0 t) P (\lambda (_: (pc3 c2 t t3)).(\lambda (H8: (ty3 g c2 t0 -t)).(ex_ind T (\lambda (t4: T).(ty3 g c2 t t4)) P (\lambda (x: T).(\lambda -(H9: (ty3 g c2 t x)).(H5 x H9 P))) (ty3_correct g c2 t0 t H8)))) +t0) t3)) (THead (Flat Cast) x t) (ty3_cast g c2 t0 t (ty3_conv g c2 t x H6 t0 +x0 H9 H12) x H6)))) (\lambda (H12: (((pc3 c2 x0 t) \to (\forall (P: +Prop).P)))).(or_intror (ex T (\lambda (t3: T).(ty3 g c2 (THead (Flat Cast) t +t0) t3))) (\forall (t3: T).((ty3 g c2 (THead (Flat Cast) t t0) t3) \to +(\forall (P: Prop).P))) (\lambda (t3: T).(\lambda (H13: (ty3 g c2 (THead +(Flat Cast) t t0) t3)).(\lambda (P: Prop).(ex3_ind T (\lambda (t4: T).(pc3 c2 +(THead (Flat Cast) t4 t) t3)) (\lambda (_: T).(ty3 g c2 t0 t)) (\lambda (t4: +T).(ty3 g c2 t t4)) P (\lambda (x2: T).(\lambda (_: (pc3 c2 (THead (Flat +Cast) x2 t) t3)).(\lambda (H15: (ty3 g c2 t0 t)).(\lambda (H16: (ty3 g c2 t +x2)).(let H_y \def (ty3_unique g c2 t x2 H16 x H6) in (let H_y0 \def +(ty3_unique g c2 t0 t H15 x0 H9) in (H12 (pc3_s c2 x0 t H_y0) P))))))) +(ty3_gen_cast g c2 t0 t t3 H13))))))) H11))))) (ty3_correct g c2 t0 x0 H9)))) +H8)) (\lambda (H8: ((\forall (t3: T).((ty3 g c2 t0 t3) \to (\forall (P: +Prop).P))))).(or_intror (ex T (\lambda (t3: T).(ty3 g c2 (THead (Flat Cast) t +t0) t3))) (\forall (t3: T).((ty3 g c2 (THead (Flat Cast) t t0) t3) \to +(\forall (P: Prop).P))) (\lambda (t3: T).(\lambda (H9: (ty3 g c2 (THead (Flat +Cast) t t0) t3)).(\lambda (P: Prop).(ex3_ind T (\lambda (t4: T).(pc3 c2 +(THead (Flat Cast) t4 t) t3)) (\lambda (_: T).(ty3 g c2 t0 t)) (\lambda (t4: +T).(ty3 g c2 t t4)) P (\lambda (x0: T).(\lambda (_: (pc3 c2 (THead (Flat +Cast) x0 t) t3)).(\lambda (H11: (ty3 g c2 t0 t)).(\lambda (_: (ty3 g c2 t +x0)).(H8 t H11 P))))) (ty3_gen_cast g c2 t0 t t3 H9))))))) H7)))) H5)) +(\lambda (H5: ((\forall (t3: T).((ty3 g c2 t t3) \to (\forall (P: +Prop).P))))).(or_intror (ex T (\lambda (t3: T).(ty3 g c2 (THead (Flat Cast) t +t0) t3))) (\forall (t3: T).((ty3 g c2 (THead (Flat Cast) t t0) t3) \to +(\forall (P: Prop).P))) (\lambda (t3: T).(\lambda (H6: (ty3 g c2 (THead (Flat +Cast) t t0) t3)).(\lambda (P: Prop).(ex3_ind T (\lambda (t4: T).(pc3 c2 +(THead (Flat Cast) t4 t) t3)) (\lambda (_: T).(ty3 g c2 t0 t)) (\lambda (t4: +T).(ty3 g c2 t t4)) P (\lambda (x0: T).(\lambda (_: (pc3 c2 (THead (Flat +Cast) x0 t) t3)).(\lambda (_: (ty3 g c2 t0 t)).(\lambda (H9: (ty3 g c2 t +x0)).(ex_ind T (\lambda (t4: T).(ty3 g c2 x0 t4)) P (\lambda (x: T).(\lambda +(_: (ty3 g c2 x0 x)).(H5 x0 H9 P))) (ty3_correct g c2 t x0 H9)))))) (ty3_gen_cast g c2 t0 t t3 H6))))))) H4))) f H2))) k H1))))))) t2))) c t1))). diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/defs.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/defs.ma index 8ddb60c91..eff4d8e7b 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/defs.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/defs.ma @@ -42,5 +42,5 @@ g c (THead (Flat Appl) w v) (THead (Flat Appl) w (THead (Bind Abst) u t))))))))) | ty3_cast: \forall (c: C).(\forall (t1: T).(\forall (t2: T).((ty3 g c t1 t2) \to (\forall (t0: T).((ty3 g c t2 t0) \to (ty3 g c (THead (Flat Cast) t2 t1) -t2)))))). +(THead (Flat Cast) t0 t2))))))). diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/fsubst0.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/fsubst0.ma index 4bc299e43..1370b3d79 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/fsubst0.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/fsubst0.ma @@ -858,99 +858,130 @@ Abbr) u)) \to (ty3 g c2 t4 t0)))))))))).(\lambda (i: nat).(\lambda (u: T).(\lambda (c2: C).(\lambda (t4: T).(\lambda (H4: (fsubst0 i u c (THead (Flat Cast) t3 t2) c2 t4)).(fsubst0_ind i u c (THead (Flat Cast) t3 t2) (\lambda (c0: C).(\lambda (t5: T).(\forall (e: C).((getl i c (CHead e (Bind -Abbr) u)) \to (ty3 g c0 t5 t3))))) (\lambda (t5: T).(\lambda (H5: (subst0 i u -(THead (Flat Cast) t3 t2) t5)).(\lambda (e: C).(\lambda (H6: (getl i c (CHead -e (Bind Abbr) u))).(or3_ind (ex2 T (\lambda (u2: T).(eq T t5 (THead (Flat -Cast) u2 t2))) (\lambda (u2: T).(subst0 i u t3 u2))) (ex2 T (\lambda (t6: -T).(eq T t5 (THead (Flat Cast) t3 t6))) (\lambda (t6: T).(subst0 (s (Flat -Cast) i) u t2 t6))) (ex3_2 T T (\lambda (u2: T).(\lambda (t6: T).(eq T t5 -(THead (Flat Cast) u2 t6)))) (\lambda (u2: T).(\lambda (_: T).(subst0 i u t3 -u2))) (\lambda (_: T).(\lambda (t6: T).(subst0 (s (Flat Cast) i) u t2 t6)))) -(ty3 g c t5 t3) (\lambda (H7: (ex2 T (\lambda (u2: T).(eq T t5 (THead (Flat -Cast) u2 t2))) (\lambda (u2: T).(subst0 i u t3 u2)))).(ex2_ind T (\lambda +Abbr) u)) \to (ty3 g c0 t5 (THead (Flat Cast) t0 t3)))))) (\lambda (t5: +T).(\lambda (H5: (subst0 i u (THead (Flat Cast) t3 t2) t5)).(\lambda (e: +C).(\lambda (H6: (getl i c (CHead e (Bind Abbr) u))).(or3_ind (ex2 T (\lambda (u2: T).(eq T t5 (THead (Flat Cast) u2 t2))) (\lambda (u2: T).(subst0 i u t3 -u2)) (ty3 g c t5 t3) (\lambda (x: T).(\lambda (H8: (eq T t5 (THead (Flat -Cast) x t2))).(\lambda (H9: (subst0 i u t3 x)).(eq_ind_r T (THead (Flat Cast) -x t2) (\lambda (t6: T).(ty3 g c t6 t3)) (ty3_conv g c t3 t0 H2 (THead (Flat -Cast) x t2) x (ty3_cast g c t2 x (ty3_conv g c x t0 (H3 i u c x (fsubst0_snd -i u c t3 x H9) e H6) t2 t3 H0 (pc3_s c t3 x (pc3_fsubst0 c t3 t3 (pc3_refl c -t3) i u c x (fsubst0_snd i u c t3 x H9) e H6))) t0 (H3 i u c x (fsubst0_snd i -u c t3 x H9) e H6)) (pc3_fsubst0 c t3 t3 (pc3_refl c t3) i u c x (fsubst0_snd -i u c t3 x H9) e H6)) t5 H8)))) H7)) (\lambda (H7: (ex2 T (\lambda (t6: -T).(eq T t5 (THead (Flat Cast) t3 t6))) (\lambda (t6: T).(subst0 (s (Flat -Cast) i) u t2 t6)))).(ex2_ind T (\lambda (t6: T).(eq T t5 (THead (Flat Cast) -t3 t6))) (\lambda (t6: T).(subst0 (s (Flat Cast) i) u t2 t6)) (ty3 g c t5 t3) -(\lambda (x: T).(\lambda (H8: (eq T t5 (THead (Flat Cast) t3 x))).(\lambda -(H9: (subst0 (s (Flat Cast) i) u t2 x)).(eq_ind_r T (THead (Flat Cast) t3 x) -(\lambda (t6: T).(ty3 g c t6 t3)) (ty3_cast g c x t3 (H1 (s (Flat Cast) i) u -c x (fsubst0_snd (s (Flat Cast) i) u c t2 x H9) e H6) t0 H2) t5 H8)))) H7)) +u2))) (ex2 T (\lambda (t6: T).(eq T t5 (THead (Flat Cast) t3 t6))) (\lambda +(t6: T).(subst0 (s (Flat Cast) i) u t2 t6))) (ex3_2 T T (\lambda (u2: +T).(\lambda (t6: T).(eq T t5 (THead (Flat Cast) u2 t6)))) (\lambda (u2: +T).(\lambda (_: T).(subst0 i u t3 u2))) (\lambda (_: T).(\lambda (t6: +T).(subst0 (s (Flat Cast) i) u t2 t6)))) (ty3 g c t5 (THead (Flat Cast) t0 +t3)) (\lambda (H7: (ex2 T (\lambda (u2: T).(eq T t5 (THead (Flat Cast) u2 +t2))) (\lambda (u2: T).(subst0 i u t3 u2)))).(ex2_ind T (\lambda (u2: T).(eq +T t5 (THead (Flat Cast) u2 t2))) (\lambda (u2: T).(subst0 i u t3 u2)) (ty3 g +c t5 (THead (Flat Cast) t0 t3)) (\lambda (x: T).(\lambda (H8: (eq T t5 (THead +(Flat Cast) x t2))).(\lambda (H9: (subst0 i u t3 x)).(eq_ind_r T (THead (Flat +Cast) x t2) (\lambda (t6: T).(ty3 g c t6 (THead (Flat Cast) t0 t3))) (ex_ind +T (\lambda (t6: T).(ty3 g c t0 t6)) (ty3 g c (THead (Flat Cast) x t2) (THead +(Flat Cast) t0 t3)) (\lambda (x0: T).(\lambda (H10: (ty3 g c t0 +x0)).(ty3_conv g c (THead (Flat Cast) t0 t3) (THead (Flat Cast) x0 t0) +(ty3_cast g c t3 t0 H2 x0 H10) (THead (Flat Cast) x t2) (THead (Flat Cast) t0 +x) (ty3_cast g c t2 x (ty3_conv g c x t0 (H3 i u c x (fsubst0_snd i u c t3 x +H9) e H6) t2 t3 H0 (pc3_s c t3 x (pc3_fsubst0 c t3 t3 (pc3_refl c t3) i u c x +(fsubst0_snd i u c t3 x H9) e H6))) t0 (H3 i u c x (fsubst0_snd i u c t3 x +H9) e H6)) (pc3_fsubst0 c (THead (Flat Cast) t0 t3) (THead (Flat Cast) t0 t3) +(pc3_refl c (THead (Flat Cast) t0 t3)) i u c (THead (Flat Cast) t0 x) +(fsubst0_snd i u c (THead (Flat Cast) t0 t3) (THead (Flat Cast) t0 x) +(subst0_snd (Flat Cast) u x t3 i H9 t0)) e H6)))) (ty3_correct g c x t0 (H3 i +u c x (fsubst0_snd i u c t3 x H9) e H6))) t5 H8)))) H7)) (\lambda (H7: (ex2 T +(\lambda (t6: T).(eq T t5 (THead (Flat Cast) t3 t6))) (\lambda (t6: +T).(subst0 (s (Flat Cast) i) u t2 t6)))).(ex2_ind T (\lambda (t6: T).(eq T t5 +(THead (Flat Cast) t3 t6))) (\lambda (t6: T).(subst0 (s (Flat Cast) i) u t2 +t6)) (ty3 g c t5 (THead (Flat Cast) t0 t3)) (\lambda (x: T).(\lambda (H8: (eq +T t5 (THead (Flat Cast) t3 x))).(\lambda (H9: (subst0 (s (Flat Cast) i) u t2 +x)).(eq_ind_r T (THead (Flat Cast) t3 x) (\lambda (t6: T).(ty3 g c t6 (THead +(Flat Cast) t0 t3))) (ty3_cast g c x t3 (H1 (s (Flat Cast) i) u c x +(fsubst0_snd (s (Flat Cast) i) u c t2 x H9) e H6) t0 H2) t5 H8)))) H7)) (\lambda (H7: (ex3_2 T T (\lambda (u2: T).(\lambda (t6: T).(eq T t5 (THead (Flat Cast) u2 t6)))) (\lambda (u2: T).(\lambda (_: T).(subst0 i u t3 u2))) (\lambda (_: T).(\lambda (t6: T).(subst0 (s (Flat Cast) i) u t2 t6))))).(ex3_2_ind T T (\lambda (u2: T).(\lambda (t6: T).(eq T t5 (THead (Flat Cast) u2 t6)))) (\lambda (u2: T).(\lambda (_: T).(subst0 i u t3 u2))) (\lambda (_: T).(\lambda (t6: T).(subst0 (s (Flat Cast) i) u t2 t6))) (ty3 g -c t5 t3) (\lambda (x0: T).(\lambda (x1: T).(\lambda (H8: (eq T t5 (THead -(Flat Cast) x0 x1))).(\lambda (H9: (subst0 i u t3 x0)).(\lambda (H10: (subst0 -(s (Flat Cast) i) u t2 x1)).(eq_ind_r T (THead (Flat Cast) x0 x1) (\lambda -(t6: T).(ty3 g c t6 t3)) (ty3_conv g c t3 t0 H2 (THead (Flat Cast) x0 x1) x0 -(ty3_cast g c x1 x0 (ty3_conv g c x0 t0 (H3 i u c x0 (fsubst0_snd i u c t3 x0 -H9) e H6) x1 t3 (H1 (s (Flat Cast) i) u c x1 (fsubst0_snd (s (Flat Cast) i) u -c t2 x1 H10) e H6) (pc3_s c t3 x0 (pc3_fsubst0 c t3 t3 (pc3_refl c t3) i u c -x0 (fsubst0_snd i u c t3 x0 H9) e H6))) t0 (H3 i u c x0 (fsubst0_snd i u c t3 -x0 H9) e H6)) (pc3_fsubst0 c t3 t3 (pc3_refl c t3) i u c x0 (fsubst0_snd i u -c t3 x0 H9) e H6)) t5 H8)))))) H7)) (subst0_gen_head (Flat Cast) u t3 t2 t5 i -H5)))))) (\lambda (c3: C).(\lambda (H5: (csubst0 i u c c3)).(\lambda (e: -C).(\lambda (H6: (getl i c (CHead e (Bind Abbr) u))).(ty3_cast g c3 t2 t3 (H1 -i u c3 t2 (fsubst0_fst i u c t2 c3 H5) e H6) t0 (H3 i u c3 t3 (fsubst0_fst i -u c t3 c3 H5) e H6)))))) (\lambda (t5: T).(\lambda (H5: (subst0 i u (THead -(Flat Cast) t3 t2) t5)).(\lambda (c3: C).(\lambda (H6: (csubst0 i u c -c3)).(\lambda (e: C).(\lambda (H7: (getl i c (CHead e (Bind Abbr) -u))).(or3_ind (ex2 T (\lambda (u2: T).(eq T t5 (THead (Flat Cast) u2 t2))) -(\lambda (u2: T).(subst0 i u t3 u2))) (ex2 T (\lambda (t6: T).(eq T t5 (THead -(Flat Cast) t3 t6))) (\lambda (t6: T).(subst0 (s (Flat Cast) i) u t2 t6))) -(ex3_2 T T (\lambda (u2: T).(\lambda (t6: T).(eq T t5 (THead (Flat Cast) u2 -t6)))) (\lambda (u2: T).(\lambda (_: T).(subst0 i u t3 u2))) (\lambda (_: -T).(\lambda (t6: T).(subst0 (s (Flat Cast) i) u t2 t6)))) (ty3 g c3 t5 t3) -(\lambda (H8: (ex2 T (\lambda (u2: T).(eq T t5 (THead (Flat Cast) u2 t2))) -(\lambda (u2: T).(subst0 i u t3 u2)))).(ex2_ind T (\lambda (u2: T).(eq T t5 -(THead (Flat Cast) u2 t2))) (\lambda (u2: T).(subst0 i u t3 u2)) (ty3 g c3 t5 -t3) (\lambda (x: T).(\lambda (H9: (eq T t5 (THead (Flat Cast) x +c t5 (THead (Flat Cast) t0 t3)) (\lambda (x0: T).(\lambda (x1: T).(\lambda +(H8: (eq T t5 (THead (Flat Cast) x0 x1))).(\lambda (H9: (subst0 i u t3 +x0)).(\lambda (H10: (subst0 (s (Flat Cast) i) u t2 x1)).(eq_ind_r T (THead +(Flat Cast) x0 x1) (\lambda (t6: T).(ty3 g c t6 (THead (Flat Cast) t0 t3))) +(ex_ind T (\lambda (t6: T).(ty3 g c t0 t6)) (ty3 g c (THead (Flat Cast) x0 +x1) (THead (Flat Cast) t0 t3)) (\lambda (x: T).(\lambda (H11: (ty3 g c t0 +x)).(ty3_conv g c (THead (Flat Cast) t0 t3) (THead (Flat Cast) x t0) +(ty3_cast g c t3 t0 H2 x H11) (THead (Flat Cast) x0 x1) (THead (Flat Cast) t0 +x0) (ty3_cast g c x1 x0 (ty3_conv g c x0 t0 (H3 i u c x0 (fsubst0_snd i u c +t3 x0 H9) e H6) x1 t3 (H1 (s (Flat Cast) i) u c x1 (fsubst0_snd (s (Flat +Cast) i) u c t2 x1 H10) e H6) (pc3_s c t3 x0 (pc3_fsubst0 c t3 t3 (pc3_refl c +t3) i u c x0 (fsubst0_snd i u c t3 x0 H9) e H6))) t0 (H3 i u c x0 +(fsubst0_snd i u c t3 x0 H9) e H6)) (pc3_fsubst0 c (THead (Flat Cast) t0 t3) +(THead (Flat Cast) t0 t3) (pc3_refl c (THead (Flat Cast) t0 t3)) i u c (THead +(Flat Cast) t0 x0) (fsubst0_snd i u c (THead (Flat Cast) t0 t3) (THead (Flat +Cast) t0 x0) (subst0_snd (Flat Cast) u x0 t3 i H9 t0)) e H6)))) (ty3_correct +g c x0 t0 (H3 i u c x0 (fsubst0_snd i u c t3 x0 H9) e H6))) t5 H8)))))) H7)) +(subst0_gen_head (Flat Cast) u t3 t2 t5 i H5)))))) (\lambda (c3: C).(\lambda +(H5: (csubst0 i u c c3)).(\lambda (e: C).(\lambda (H6: (getl i c (CHead e +(Bind Abbr) u))).(ty3_cast g c3 t2 t3 (H1 i u c3 t2 (fsubst0_fst i u c t2 c3 +H5) e H6) t0 (H3 i u c3 t3 (fsubst0_fst i u c t3 c3 H5) e H6)))))) (\lambda +(t5: T).(\lambda (H5: (subst0 i u (THead (Flat Cast) t3 t2) t5)).(\lambda +(c3: C).(\lambda (H6: (csubst0 i u c c3)).(\lambda (e: C).(\lambda (H7: (getl +i c (CHead e (Bind Abbr) u))).(or3_ind (ex2 T (\lambda (u2: T).(eq T t5 +(THead (Flat Cast) u2 t2))) (\lambda (u2: T).(subst0 i u t3 u2))) (ex2 T +(\lambda (t6: T).(eq T t5 (THead (Flat Cast) t3 t6))) (\lambda (t6: +T).(subst0 (s (Flat Cast) i) u t2 t6))) (ex3_2 T T (\lambda (u2: T).(\lambda +(t6: T).(eq T t5 (THead (Flat Cast) u2 t6)))) (\lambda (u2: T).(\lambda (_: +T).(subst0 i u t3 u2))) (\lambda (_: T).(\lambda (t6: T).(subst0 (s (Flat +Cast) i) u t2 t6)))) (ty3 g c3 t5 (THead (Flat Cast) t0 t3)) (\lambda (H8: +(ex2 T (\lambda (u2: T).(eq T t5 (THead (Flat Cast) u2 t2))) (\lambda (u2: +T).(subst0 i u t3 u2)))).(ex2_ind T (\lambda (u2: T).(eq T t5 (THead (Flat +Cast) u2 t2))) (\lambda (u2: T).(subst0 i u t3 u2)) (ty3 g c3 t5 (THead (Flat +Cast) t0 t3)) (\lambda (x: T).(\lambda (H9: (eq T t5 (THead (Flat Cast) x t2))).(\lambda (H10: (subst0 i u t3 x)).(eq_ind_r T (THead (Flat Cast) x t2) -(\lambda (t6: T).(ty3 g c3 t6 t3)) (ty3_conv g c3 t3 t0 (H3 i u c3 t3 -(fsubst0_fst i u c t3 c3 H6) e H7) (THead (Flat Cast) x t2) x (ty3_cast g c3 -t2 x (ty3_conv g c3 x t0 (H3 i u c3 x (fsubst0_both i u c t3 x H10 c3 H6) e -H7) t2 t3 (H1 i u c3 t2 (fsubst0_fst i u c t2 c3 H6) e H7) (pc3_s c3 t3 x -(pc3_fsubst0 c t3 t3 (pc3_refl c t3) i u c3 x (fsubst0_both i u c t3 x H10 c3 -H6) e H7))) t0 (H3 i u c3 x (fsubst0_both i u c t3 x H10 c3 H6) e H7)) -(pc3_fsubst0 c t3 t3 (pc3_refl c t3) i u c3 x (fsubst0_both i u c t3 x H10 c3 -H6) e H7)) t5 H9)))) H8)) (\lambda (H8: (ex2 T (\lambda (t6: T).(eq T t5 -(THead (Flat Cast) t3 t6))) (\lambda (t6: T).(subst0 (s (Flat Cast) i) u t2 +(\lambda (t6: T).(ty3 g c3 t6 (THead (Flat Cast) t0 t3))) (ex_ind T (\lambda +(t6: T).(ty3 g c3 t0 t6)) (ty3 g c3 (THead (Flat Cast) x t2) (THead (Flat +Cast) t0 t3)) (\lambda (x0: T).(\lambda (H11: (ty3 g c3 t0 x0)).(ty3_conv g +c3 (THead (Flat Cast) t0 t3) (THead (Flat Cast) x0 t0) (ty3_cast g c3 t3 t0 +(H3 i u c3 t3 (fsubst0_fst i u c t3 c3 H6) e H7) x0 H11) (THead (Flat Cast) x +t2) (THead (Flat Cast) t0 x) (ty3_cast g c3 t2 x (ty3_conv g c3 x t0 (H3 i u +c3 x (fsubst0_both i u c t3 x H10 c3 H6) e H7) t2 t3 (H1 i u c3 t2 +(fsubst0_fst i u c t2 c3 H6) e H7) (pc3_s c3 t3 x (pc3_fsubst0 c t3 t3 +(pc3_refl c t3) i u c3 x (fsubst0_both i u c t3 x H10 c3 H6) e H7))) t0 (H3 i +u c3 x (fsubst0_both i u c t3 x H10 c3 H6) e H7)) (pc3_fsubst0 c (THead (Flat +Cast) t0 t3) (THead (Flat Cast) t0 t3) (pc3_refl c (THead (Flat Cast) t0 t3)) +i u c3 (THead (Flat Cast) t0 x) (fsubst0_both i u c (THead (Flat Cast) t0 t3) +(THead (Flat Cast) t0 x) (subst0_snd (Flat Cast) u x t3 i H10 t0) c3 H6) e +H7)))) (ty3_correct g c3 t3 t0 (H3 i u c3 t3 (fsubst0_fst i u c t3 c3 H6) e +H7))) t5 H9)))) H8)) (\lambda (H8: (ex2 T (\lambda (t6: T).(eq T t5 (THead +(Flat Cast) t3 t6))) (\lambda (t6: T).(subst0 (s (Flat Cast) i) u t2 t6)))).(ex2_ind T (\lambda (t6: T).(eq T t5 (THead (Flat Cast) t3 t6))) -(\lambda (t6: T).(subst0 (s (Flat Cast) i) u t2 t6)) (ty3 g c3 t5 t3) -(\lambda (x: T).(\lambda (H9: (eq T t5 (THead (Flat Cast) t3 x))).(\lambda -(H10: (subst0 (s (Flat Cast) i) u t2 x)).(eq_ind_r T (THead (Flat Cast) t3 x) -(\lambda (t6: T).(ty3 g c3 t6 t3)) (ty3_cast g c3 x t3 (H1 i u c3 x -(fsubst0_both i u c t2 x H10 c3 H6) e H7) t0 (H3 i u c3 t3 (fsubst0_fst i u c -t3 c3 H6) e H7)) t5 H9)))) H8)) (\lambda (H8: (ex3_2 T T (\lambda (u2: -T).(\lambda (t6: T).(eq T t5 (THead (Flat Cast) u2 t6)))) (\lambda (u2: -T).(\lambda (_: T).(subst0 i u t3 u2))) (\lambda (_: T).(\lambda (t6: -T).(subst0 (s (Flat Cast) i) u t2 t6))))).(ex3_2_ind T T (\lambda (u2: -T).(\lambda (t6: T).(eq T t5 (THead (Flat Cast) u2 t6)))) (\lambda (u2: -T).(\lambda (_: T).(subst0 i u t3 u2))) (\lambda (_: T).(\lambda (t6: -T).(subst0 (s (Flat Cast) i) u t2 t6))) (ty3 g c3 t5 t3) (\lambda (x0: -T).(\lambda (x1: T).(\lambda (H9: (eq T t5 (THead (Flat Cast) x0 -x1))).(\lambda (H10: (subst0 i u t3 x0)).(\lambda (H11: (subst0 (s (Flat -Cast) i) u t2 x1)).(eq_ind_r T (THead (Flat Cast) x0 x1) (\lambda (t6: -T).(ty3 g c3 t6 t3)) (ty3_conv g c3 t3 t0 (H3 i u c3 t3 (fsubst0_fst i u c t3 -c3 H6) e H7) (THead (Flat Cast) x0 x1) x0 (ty3_cast g c3 x1 x0 (ty3_conv g c3 -x0 t0 (H3 i u c3 x0 (fsubst0_both i u c t3 x0 H10 c3 H6) e H7) x1 t3 (H1 i u -c3 x1 (fsubst0_both i u c t2 x1 H11 c3 H6) e H7) (pc3_s c3 t3 x0 (pc3_fsubst0 -c t3 t3 (pc3_refl c t3) i u c3 x0 (fsubst0_both i u c t3 x0 H10 c3 H6) e -H7))) t0 (H3 i u c3 x0 (fsubst0_both i u c t3 x0 H10 c3 H6) e H7)) -(pc3_fsubst0 c t3 t3 (pc3_refl c t3) i u c3 x0 (fsubst0_both i u c t3 x0 H10 -c3 H6) e H7)) t5 H9)))))) H8)) (subst0_gen_head (Flat Cast) u t3 t2 t5 i -H5)))))))) c2 t4 H4)))))))))))))) c1 t1 t H))))). +(\lambda (t6: T).(subst0 (s (Flat Cast) i) u t2 t6)) (ty3 g c3 t5 (THead +(Flat Cast) t0 t3)) (\lambda (x: T).(\lambda (H9: (eq T t5 (THead (Flat Cast) +t3 x))).(\lambda (H10: (subst0 (s (Flat Cast) i) u t2 x)).(eq_ind_r T (THead +(Flat Cast) t3 x) (\lambda (t6: T).(ty3 g c3 t6 (THead (Flat Cast) t0 t3))) +(ty3_cast g c3 x t3 (H1 i u c3 x (fsubst0_both i u c t2 x H10 c3 H6) e H7) t0 +(H3 i u c3 t3 (fsubst0_fst i u c t3 c3 H6) e H7)) t5 H9)))) H8)) (\lambda +(H8: (ex3_2 T T (\lambda (u2: T).(\lambda (t6: T).(eq T t5 (THead (Flat Cast) +u2 t6)))) (\lambda (u2: T).(\lambda (_: T).(subst0 i u t3 u2))) (\lambda (_: +T).(\lambda (t6: T).(subst0 (s (Flat Cast) i) u t2 t6))))).(ex3_2_ind T T +(\lambda (u2: T).(\lambda (t6: T).(eq T t5 (THead (Flat Cast) u2 t6)))) +(\lambda (u2: T).(\lambda (_: T).(subst0 i u t3 u2))) (\lambda (_: +T).(\lambda (t6: T).(subst0 (s (Flat Cast) i) u t2 t6))) (ty3 g c3 t5 (THead +(Flat Cast) t0 t3)) (\lambda (x0: T).(\lambda (x1: T).(\lambda (H9: (eq T t5 +(THead (Flat Cast) x0 x1))).(\lambda (H10: (subst0 i u t3 x0)).(\lambda (H11: +(subst0 (s (Flat Cast) i) u t2 x1)).(eq_ind_r T (THead (Flat Cast) x0 x1) +(\lambda (t6: T).(ty3 g c3 t6 (THead (Flat Cast) t0 t3))) (ex_ind T (\lambda +(t6: T).(ty3 g c3 t0 t6)) (ty3 g c3 (THead (Flat Cast) x0 x1) (THead (Flat +Cast) t0 t3)) (\lambda (x: T).(\lambda (H12: (ty3 g c3 t0 x)).(ty3_conv g c3 +(THead (Flat Cast) t0 t3) (THead (Flat Cast) x t0) (ty3_cast g c3 t3 t0 (H3 i +u c3 t3 (fsubst0_fst i u c t3 c3 H6) e H7) x H12) (THead (Flat Cast) x0 x1) +(THead (Flat Cast) t0 x0) (ty3_cast g c3 x1 x0 (ty3_conv g c3 x0 t0 (H3 i u +c3 x0 (fsubst0_both i u c t3 x0 H10 c3 H6) e H7) x1 t3 (H1 i u c3 x1 +(fsubst0_both i u c t2 x1 H11 c3 H6) e H7) (pc3_s c3 t3 x0 (pc3_fsubst0 c t3 +t3 (pc3_refl c t3) i u c3 x0 (fsubst0_both i u c t3 x0 H10 c3 H6) e H7))) t0 +(H3 i u c3 x0 (fsubst0_both i u c t3 x0 H10 c3 H6) e H7)) (pc3_fsubst0 c +(THead (Flat Cast) t0 t3) (THead (Flat Cast) t0 t3) (pc3_refl c (THead (Flat +Cast) t0 t3)) i u c3 (THead (Flat Cast) t0 x0) (fsubst0_both i u c (THead +(Flat Cast) t0 t3) (THead (Flat Cast) t0 x0) (subst0_snd (Flat Cast) u x0 t3 +i H10 t0) c3 H6) e H7)))) (ty3_correct g c3 t3 t0 (H3 i u c3 t3 (fsubst0_fst +i u c t3 c3 H6) e H7))) t5 H9)))))) H8)) (subst0_gen_head (Flat Cast) u t3 t2 +t5 i H5)))))))) c2 t4 H4)))))))))))))) c1 t1 t H))))). theorem ty3_csubst0: \forall (g: G).(\forall (c1: C).(\forall (t1: T).(\forall (t2: T).((ty3 g c1 diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/fwd.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/fwd.ma index 3e9846516..5267f5c6a 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/fwd.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/fwd.ma @@ -87,8 +87,8 @@ t1 (TSort n)) \to (pc3 c0 (TSort (next g n)) t2)))).(\lambda (t0: T).(\lambda n))).(let H6 \def (eq_ind T (THead (Flat Cast) t2 t1) (\lambda (ee: T).(match ee in T return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow False | (THead _ _ _) \Rightarrow True])) I (TSort n) -H5) in (False_ind (pc3 c0 (TSort (next g n)) t2) H6))))))))))) c y x H0))) -H))))). +H5) in (False_ind (pc3 c0 (TSort (next g n)) (THead (Flat Cast) t0 t2)) +H6))))))))))) c y x H0))) H))))). theorem ty3_gen_lref: \forall (g: G).(\forall (c: C).(\forall (x: T).(\forall (n: nat).((ty3 g c @@ -383,12 +383,13 @@ Cast) t2 t1) (\lambda (ee: T).(match ee in T return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow False | (THead _ _ _) \Rightarrow True])) I (TLRef n) H5) in (False_ind (or (ex3_3 C T T (\lambda (_: C).(\lambda (_: T).(\lambda (t: T).(pc3 c0 (lift (S n) O t) -t2)))) (\lambda (e: C).(\lambda (u: T).(\lambda (_: T).(getl n c0 (CHead e -(Bind Abbr) u))))) (\lambda (e: C).(\lambda (u: T).(\lambda (t: T).(ty3 g e u -t))))) (ex3_3 C T T (\lambda (_: C).(\lambda (u: T).(\lambda (_: T).(pc3 c0 -(lift (S n) O u) t2)))) (\lambda (e: C).(\lambda (u: T).(\lambda (_: T).(getl -n c0 (CHead e (Bind Abst) u))))) (\lambda (e: C).(\lambda (u: T).(\lambda (t: -T).(ty3 g e u t)))))) H6))))))))))) c y x H0))) H))))). +(THead (Flat Cast) t0 t2))))) (\lambda (e: C).(\lambda (u: T).(\lambda (_: +T).(getl n c0 (CHead e (Bind Abbr) u))))) (\lambda (e: C).(\lambda (u: +T).(\lambda (t: T).(ty3 g e u t))))) (ex3_3 C T T (\lambda (_: C).(\lambda +(u: T).(\lambda (_: T).(pc3 c0 (lift (S n) O u) (THead (Flat Cast) t0 t2))))) +(\lambda (e: C).(\lambda (u: T).(\lambda (_: T).(getl n c0 (CHead e (Bind +Abst) u))))) (\lambda (e: C).(\lambda (u: T).(\lambda (t: T).(ty3 g e u +t)))))) H6))))))))))) c y x H0))) H))))). theorem ty3_gen_bind: \forall (g: G).(\forall (b: B).(\forall (c: C).(\forall (u: T).(\forall (t1: @@ -638,11 +639,11 @@ _) \Rightarrow False | (TLRef _) \Rightarrow False | (THead k _ _) \Rightarrow (match k in K return (\lambda (_: K).Prop) with [(Bind _) \Rightarrow False | (Flat _) \Rightarrow True])])) I (THead (Bind b) u t1) H5) in (False_ind (ex4_3 T T T (\lambda (t4: T).(\lambda (_: T).(\lambda (_: -T).(pc3 c0 (THead (Bind b) u t4) t2)))) (\lambda (_: T).(\lambda (t: -T).(\lambda (_: T).(ty3 g c0 u t)))) (\lambda (t4: T).(\lambda (_: -T).(\lambda (_: T).(ty3 g (CHead c0 (Bind b) u) t1 t4)))) (\lambda (t4: -T).(\lambda (_: T).(\lambda (t5: T).(ty3 g (CHead c0 (Bind b) u) t4 t5))))) -H6))))))))))) c y x H0))) H))))))). +T).(pc3 c0 (THead (Bind b) u t4) (THead (Flat Cast) t3 t2))))) (\lambda (_: +T).(\lambda (t: T).(\lambda (_: T).(ty3 g c0 u t)))) (\lambda (t4: +T).(\lambda (_: T).(\lambda (_: T).(ty3 g (CHead c0 (Bind b) u) t1 t4)))) +(\lambda (t4: T).(\lambda (_: T).(\lambda (t5: T).(ty3 g (CHead c0 (Bind b) +u) t4 t5))))) H6))))))))))) c y x H0))) H))))))). theorem ty3_gen_appl: \forall (g: G).(\forall (c: C).(\forall (w: T).(\forall (v: T).(\forall (x: @@ -810,105 +811,144 @@ Abst) u t)))) (\lambda (u: T).(\lambda (_: T).(ty3 g c0 w u))))))).(\lambda in F return (\lambda (_: F).Prop) with [Appl \Rightarrow False | Cast \Rightarrow True])])])) I (THead (Flat Appl) w v) H5) in (False_ind (ex3_2 T T (\lambda (u: T).(\lambda (t: T).(pc3 c0 (THead (Flat Appl) w (THead (Bind -Abst) u t)) t2))) (\lambda (u: T).(\lambda (t: T).(ty3 g c0 v (THead (Bind -Abst) u t)))) (\lambda (u: T).(\lambda (_: T).(ty3 g c0 w u)))) H6))))))))))) -c y x H0))) H)))))). +Abst) u t)) (THead (Flat Cast) t0 t2)))) (\lambda (u: T).(\lambda (t: T).(ty3 +g c0 v (THead (Bind Abst) u t)))) (\lambda (u: T).(\lambda (_: T).(ty3 g c0 w +u)))) H6))))))))))) c y x H0))) H)))))). theorem ty3_gen_cast: \forall (g: G).(\forall (c: C).(\forall (t1: T).(\forall (t2: T).(\forall -(x: T).((ty3 g c (THead (Flat Cast) t2 t1) x) \to (land (pc3 c t2 x) (ty3 g c -t1 t2))))))) +(x: T).((ty3 g c (THead (Flat Cast) t2 t1) x) \to (ex3 T (\lambda (t0: +T).(pc3 c (THead (Flat Cast) t0 t2) x)) (\lambda (_: T).(ty3 g c t1 t2)) +(\lambda (t0: T).(ty3 g c t2 t0)))))))) \def \lambda (g: G).(\lambda (c: C).(\lambda (t1: T).(\lambda (t2: T).(\lambda (x: T).(\lambda (H: (ty3 g c (THead (Flat Cast) t2 t1) x)).(insert_eq T -(THead (Flat Cast) t2 t1) (\lambda (t: T).(ty3 g c t x)) (land (pc3 c t2 x) -(ty3 g c t1 t2)) (\lambda (y: T).(\lambda (H0: (ty3 g c y x)).(ty3_ind g -(\lambda (c0: C).(\lambda (t: T).(\lambda (t0: T).((eq T t (THead (Flat Cast) -t2 t1)) \to (land (pc3 c0 t2 t0) (ty3 g c0 t1 t2)))))) (\lambda (c0: -C).(\lambda (t0: T).(\lambda (t: T).(\lambda (_: (ty3 g c0 t0 t)).(\lambda -(_: (((eq T t0 (THead (Flat Cast) t2 t1)) \to (land (pc3 c0 t2 t) (ty3 g c0 -t1 t2))))).(\lambda (u: T).(\lambda (t3: T).(\lambda (H3: (ty3 g c0 u -t3)).(\lambda (H4: (((eq T u (THead (Flat Cast) t2 t1)) \to (land (pc3 c0 t2 -t3) (ty3 g c0 t1 t2))))).(\lambda (H5: (pc3 c0 t3 t0)).(\lambda (H6: (eq T u -(THead (Flat Cast) t2 t1))).(let H7 \def (f_equal T T (\lambda (e: T).e) u -(THead (Flat Cast) t2 t1) H6) in (let H8 \def (eq_ind T u (\lambda (t4: -T).((eq T t4 (THead (Flat Cast) t2 t1)) \to (land (pc3 c0 t2 t3) (ty3 g c0 t1 -t2)))) H4 (THead (Flat Cast) t2 t1) H7) in (let H9 \def (eq_ind T u (\lambda -(t4: T).(ty3 g c0 t4 t3)) H3 (THead (Flat Cast) t2 t1) H7) in (let H10 \def -(H8 (refl_equal T (THead (Flat Cast) t2 t1))) in (and_ind (pc3 c0 t2 t3) (ty3 -g c0 t1 t2) (land (pc3 c0 t2 t0) (ty3 g c0 t1 t2)) (\lambda (H11: (pc3 c0 t2 -t3)).(\lambda (H12: (ty3 g c0 t1 t2)).(conj (pc3 c0 t2 t0) (ty3 g c0 t1 t2) -(pc3_t t3 c0 t2 H11 t0 H5) H12))) H10)))))))))))))))) (\lambda (c0: -C).(\lambda (m: nat).(\lambda (H1: (eq T (TSort m) (THead (Flat Cast) t2 -t1))).(let H2 \def (eq_ind T (TSort m) (\lambda (ee: T).(match ee in T return -(\lambda (_: T).Prop) with [(TSort _) \Rightarrow True | (TLRef _) -\Rightarrow False | (THead _ _ _) \Rightarrow False])) I (THead (Flat Cast) -t2 t1) H1) in (False_ind (land (pc3 c0 t2 (TSort (next g m))) (ty3 g c0 t1 -t2)) H2))))) (\lambda (n: nat).(\lambda (c0: C).(\lambda (d: C).(\lambda (u: -T).(\lambda (_: (getl n c0 (CHead d (Bind Abbr) u))).(\lambda (t: T).(\lambda -(_: (ty3 g d u t)).(\lambda (_: (((eq T u (THead (Flat Cast) t2 t1)) \to -(land (pc3 d t2 t) (ty3 g d t1 t2))))).(\lambda (H4: (eq T (TLRef n) (THead +(THead (Flat Cast) t2 t1) (\lambda (t: T).(ty3 g c t x)) (ex3 T (\lambda (t0: +T).(pc3 c (THead (Flat Cast) t0 t2) x)) (\lambda (_: T).(ty3 g c t1 t2)) +(\lambda (t0: T).(ty3 g c t2 t0))) (\lambda (y: T).(\lambda (H0: (ty3 g c y +x)).(ty3_ind g (\lambda (c0: C).(\lambda (t: T).(\lambda (t0: T).((eq T t +(THead (Flat Cast) t2 t1)) \to (ex3 T (\lambda (t3: T).(pc3 c0 (THead (Flat +Cast) t3 t2) t0)) (\lambda (_: T).(ty3 g c0 t1 t2)) (\lambda (t3: T).(ty3 g +c0 t2 t3))))))) (\lambda (c0: C).(\lambda (t0: T).(\lambda (t: T).(\lambda +(_: (ty3 g c0 t0 t)).(\lambda (_: (((eq T t0 (THead (Flat Cast) t2 t1)) \to +(ex3 T (\lambda (t3: T).(pc3 c0 (THead (Flat Cast) t3 t2) t)) (\lambda (_: +T).(ty3 g c0 t1 t2)) (\lambda (t3: T).(ty3 g c0 t2 t3)))))).(\lambda (u: +T).(\lambda (t3: T).(\lambda (H3: (ty3 g c0 u t3)).(\lambda (H4: (((eq T u +(THead (Flat Cast) t2 t1)) \to (ex3 T (\lambda (t4: T).(pc3 c0 (THead (Flat +Cast) t4 t2) t3)) (\lambda (_: T).(ty3 g c0 t1 t2)) (\lambda (t4: T).(ty3 g +c0 t2 t4)))))).(\lambda (H5: (pc3 c0 t3 t0)).(\lambda (H6: (eq T u (THead +(Flat Cast) t2 t1))).(let H7 \def (f_equal T T (\lambda (e: T).e) u (THead +(Flat Cast) t2 t1) H6) in (let H8 \def (eq_ind T u (\lambda (t4: T).((eq T t4 +(THead (Flat Cast) t2 t1)) \to (ex3 T (\lambda (t5: T).(pc3 c0 (THead (Flat +Cast) t5 t2) t3)) (\lambda (_: T).(ty3 g c0 t1 t2)) (\lambda (t5: T).(ty3 g +c0 t2 t5))))) H4 (THead (Flat Cast) t2 t1) H7) in (let H9 \def (eq_ind T u +(\lambda (t4: T).(ty3 g c0 t4 t3)) H3 (THead (Flat Cast) t2 t1) H7) in (let +H10 \def (H8 (refl_equal T (THead (Flat Cast) t2 t1))) in (ex3_ind T (\lambda +(t4: T).(pc3 c0 (THead (Flat Cast) t4 t2) t3)) (\lambda (_: T).(ty3 g c0 t1 +t2)) (\lambda (t4: T).(ty3 g c0 t2 t4)) (ex3 T (\lambda (t4: T).(pc3 c0 +(THead (Flat Cast) t4 t2) t0)) (\lambda (_: T).(ty3 g c0 t1 t2)) (\lambda +(t4: T).(ty3 g c0 t2 t4))) (\lambda (x0: T).(\lambda (H11: (pc3 c0 (THead +(Flat Cast) x0 t2) t3)).(\lambda (H12: (ty3 g c0 t1 t2)).(\lambda (H13: (ty3 +g c0 t2 x0)).(ex3_intro T (\lambda (t4: T).(pc3 c0 (THead (Flat Cast) t4 t2) +t0)) (\lambda (_: T).(ty3 g c0 t1 t2)) (\lambda (t4: T).(ty3 g c0 t2 t4)) x0 +(pc3_t t3 c0 (THead (Flat Cast) x0 t2) H11 t0 H5) H12 H13))))) +H10)))))))))))))))) (\lambda (c0: C).(\lambda (m: nat).(\lambda (H1: (eq T +(TSort m) (THead (Flat Cast) t2 t1))).(let H2 \def (eq_ind T (TSort m) +(\lambda (ee: T).(match ee in T return (\lambda (_: T).Prop) with [(TSort _) +\Rightarrow True | (TLRef _) \Rightarrow False | (THead _ _ _) \Rightarrow +False])) I (THead (Flat Cast) t2 t1) H1) in (False_ind (ex3 T (\lambda (t0: +T).(pc3 c0 (THead (Flat Cast) t0 t2) (TSort (next g m)))) (\lambda (_: +T).(ty3 g c0 t1 t2)) (\lambda (t0: T).(ty3 g c0 t2 t0))) H2))))) (\lambda (n: +nat).(\lambda (c0: C).(\lambda (d: C).(\lambda (u: T).(\lambda (_: (getl n c0 +(CHead d (Bind Abbr) u))).(\lambda (t: T).(\lambda (_: (ty3 g d u +t)).(\lambda (_: (((eq T u (THead (Flat Cast) t2 t1)) \to (ex3 T (\lambda +(t0: T).(pc3 d (THead (Flat Cast) t0 t2) t)) (\lambda (_: T).(ty3 g d t1 t2)) +(\lambda (t0: T).(ty3 g d t2 t0)))))).(\lambda (H4: (eq T (TLRef n) (THead (Flat Cast) t2 t1))).(let H5 \def (eq_ind T (TLRef n) (\lambda (ee: T).(match ee in T return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow True | (THead _ _ _) \Rightarrow False])) I (THead -(Flat Cast) t2 t1) H4) in (False_ind (land (pc3 c0 t2 (lift (S n) O t)) (ty3 -g c0 t1 t2)) H5))))))))))) (\lambda (n: nat).(\lambda (c0: C).(\lambda (d: -C).(\lambda (u: T).(\lambda (_: (getl n c0 (CHead d (Bind Abst) u))).(\lambda -(t: T).(\lambda (_: (ty3 g d u t)).(\lambda (_: (((eq T u (THead (Flat Cast) -t2 t1)) \to (land (pc3 d t2 t) (ty3 g d t1 t2))))).(\lambda (H4: (eq T (TLRef -n) (THead (Flat Cast) t2 t1))).(let H5 \def (eq_ind T (TLRef n) (\lambda (ee: -T).(match ee in T return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow -False | (TLRef _) \Rightarrow True | (THead _ _ _) \Rightarrow False])) I -(THead (Flat Cast) t2 t1) H4) in (False_ind (land (pc3 c0 t2 (lift (S n) O -u)) (ty3 g c0 t1 t2)) H5))))))))))) (\lambda (c0: C).(\lambda (u: T).(\lambda +(Flat Cast) t2 t1) H4) in (False_ind (ex3 T (\lambda (t0: T).(pc3 c0 (THead +(Flat Cast) t0 t2) (lift (S n) O t))) (\lambda (_: T).(ty3 g c0 t1 t2)) +(\lambda (t0: T).(ty3 g c0 t2 t0))) H5))))))))))) (\lambda (n: nat).(\lambda +(c0: C).(\lambda (d: C).(\lambda (u: T).(\lambda (_: (getl n c0 (CHead d +(Bind Abst) u))).(\lambda (t: T).(\lambda (_: (ty3 g d u t)).(\lambda (_: +(((eq T u (THead (Flat Cast) t2 t1)) \to (ex3 T (\lambda (t0: T).(pc3 d +(THead (Flat Cast) t0 t2) t)) (\lambda (_: T).(ty3 g d t1 t2)) (\lambda (t0: +T).(ty3 g d t2 t0)))))).(\lambda (H4: (eq T (TLRef n) (THead (Flat Cast) t2 +t1))).(let H5 \def (eq_ind T (TLRef n) (\lambda (ee: T).(match ee in T return +(\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef _) +\Rightarrow True | (THead _ _ _) \Rightarrow False])) I (THead (Flat Cast) t2 +t1) H4) in (False_ind (ex3 T (\lambda (t0: T).(pc3 c0 (THead (Flat Cast) t0 +t2) (lift (S n) O u))) (\lambda (_: T).(ty3 g c0 t1 t2)) (\lambda (t0: +T).(ty3 g c0 t2 t0))) H5))))))))))) (\lambda (c0: C).(\lambda (u: T).(\lambda (t: T).(\lambda (_: (ty3 g c0 u t)).(\lambda (_: (((eq T u (THead (Flat Cast) -t2 t1)) \to (land (pc3 c0 t2 t) (ty3 g c0 t1 t2))))).(\lambda (b: B).(\lambda -(t0: T).(\lambda (t3: T).(\lambda (_: (ty3 g (CHead c0 (Bind b) u) t0 -t3)).(\lambda (_: (((eq T t0 (THead (Flat Cast) t2 t1)) \to (land (pc3 (CHead -c0 (Bind b) u) t2 t3) (ty3 g (CHead c0 (Bind b) u) t1 t2))))).(\lambda (t4: +t2 t1)) \to (ex3 T (\lambda (t0: T).(pc3 c0 (THead (Flat Cast) t0 t2) t)) +(\lambda (_: T).(ty3 g c0 t1 t2)) (\lambda (t0: T).(ty3 g c0 t2 +t0)))))).(\lambda (b: B).(\lambda (t0: T).(\lambda (t3: T).(\lambda (_: (ty3 +g (CHead c0 (Bind b) u) t0 t3)).(\lambda (_: (((eq T t0 (THead (Flat Cast) t2 +t1)) \to (ex3 T (\lambda (t4: T).(pc3 (CHead c0 (Bind b) u) (THead (Flat +Cast) t4 t2) t3)) (\lambda (_: T).(ty3 g (CHead c0 (Bind b) u) t1 t2)) +(\lambda (t4: T).(ty3 g (CHead c0 (Bind b) u) t2 t4)))))).(\lambda (t4: T).(\lambda (_: (ty3 g (CHead c0 (Bind b) u) t3 t4)).(\lambda (_: (((eq T t3 -(THead (Flat Cast) t2 t1)) \to (land (pc3 (CHead c0 (Bind b) u) t2 t4) (ty3 g -(CHead c0 (Bind b) u) t1 t2))))).(\lambda (H7: (eq T (THead (Bind b) u t0) -(THead (Flat Cast) t2 t1))).(let H8 \def (eq_ind T (THead (Bind b) u t0) -(\lambda (ee: T).(match ee in T return (\lambda (_: T).Prop) with [(TSort _) -\Rightarrow False | (TLRef _) \Rightarrow False | (THead k _ _) \Rightarrow -(match k in K return (\lambda (_: K).Prop) with [(Bind _) \Rightarrow True | -(Flat _) \Rightarrow False])])) I (THead (Flat Cast) t2 t1) H7) in (False_ind -(land (pc3 c0 t2 (THead (Bind b) u t3)) (ty3 g c0 t1 t2)) H8)))))))))))))))) +(THead (Flat Cast) t2 t1)) \to (ex3 T (\lambda (t5: T).(pc3 (CHead c0 (Bind +b) u) (THead (Flat Cast) t5 t2) t4)) (\lambda (_: T).(ty3 g (CHead c0 (Bind +b) u) t1 t2)) (\lambda (t5: T).(ty3 g (CHead c0 (Bind b) u) t2 +t5)))))).(\lambda (H7: (eq T (THead (Bind b) u t0) (THead (Flat Cast) t2 +t1))).(let H8 \def (eq_ind T (THead (Bind b) u t0) (\lambda (ee: T).(match ee +in T return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef +_) \Rightarrow False | (THead k _ _) \Rightarrow (match k in K return +(\lambda (_: K).Prop) with [(Bind _) \Rightarrow True | (Flat _) \Rightarrow +False])])) I (THead (Flat Cast) t2 t1) H7) in (False_ind (ex3 T (\lambda (t5: +T).(pc3 c0 (THead (Flat Cast) t5 t2) (THead (Bind b) u t3))) (\lambda (_: +T).(ty3 g c0 t1 t2)) (\lambda (t5: T).(ty3 g c0 t2 t5))) H8)))))))))))))))) (\lambda (c0: C).(\lambda (w: T).(\lambda (u: T).(\lambda (_: (ty3 g c0 w -u)).(\lambda (_: (((eq T w (THead (Flat Cast) t2 t1)) \to (land (pc3 c0 t2 u) -(ty3 g c0 t1 t2))))).(\lambda (v: T).(\lambda (t: T).(\lambda (_: (ty3 g c0 v -(THead (Bind Abst) u t))).(\lambda (_: (((eq T v (THead (Flat Cast) t2 t1)) -\to (land (pc3 c0 t2 (THead (Bind Abst) u t)) (ty3 g c0 t1 t2))))).(\lambda -(H5: (eq T (THead (Flat Appl) w v) (THead (Flat Cast) t2 t1))).(let H6 \def -(eq_ind T (THead (Flat Appl) w v) (\lambda (ee: T).(match ee in T return -(\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef _) -\Rightarrow False | (THead k _ _) \Rightarrow (match k in K return (\lambda -(_: K).Prop) with [(Bind _) \Rightarrow False | (Flat f) \Rightarrow (match f -in F return (\lambda (_: F).Prop) with [Appl \Rightarrow True | Cast -\Rightarrow False])])])) I (THead (Flat Cast) t2 t1) H5) in (False_ind (land -(pc3 c0 t2 (THead (Flat Appl) w (THead (Bind Abst) u t))) (ty3 g c0 t1 t2)) -H6)))))))))))) (\lambda (c0: C).(\lambda (t0: T).(\lambda (t3: T).(\lambda -(H1: (ty3 g c0 t0 t3)).(\lambda (H2: (((eq T t0 (THead (Flat Cast) t2 t1)) -\to (land (pc3 c0 t2 t3) (ty3 g c0 t1 t2))))).(\lambda (t4: T).(\lambda (H3: +u)).(\lambda (_: (((eq T w (THead (Flat Cast) t2 t1)) \to (ex3 T (\lambda +(t0: T).(pc3 c0 (THead (Flat Cast) t0 t2) u)) (\lambda (_: T).(ty3 g c0 t1 +t2)) (\lambda (t0: T).(ty3 g c0 t2 t0)))))).(\lambda (v: T).(\lambda (t: +T).(\lambda (_: (ty3 g c0 v (THead (Bind Abst) u t))).(\lambda (_: (((eq T v +(THead (Flat Cast) t2 t1)) \to (ex3 T (\lambda (t0: T).(pc3 c0 (THead (Flat +Cast) t0 t2) (THead (Bind Abst) u t))) (\lambda (_: T).(ty3 g c0 t1 t2)) +(\lambda (t0: T).(ty3 g c0 t2 t0)))))).(\lambda (H5: (eq T (THead (Flat Appl) +w v) (THead (Flat Cast) t2 t1))).(let H6 \def (eq_ind T (THead (Flat Appl) w +v) (\lambda (ee: T).(match ee in T return (\lambda (_: T).Prop) with [(TSort +_) \Rightarrow False | (TLRef _) \Rightarrow False | (THead k _ _) +\Rightarrow (match k in K return (\lambda (_: K).Prop) with [(Bind _) +\Rightarrow False | (Flat f) \Rightarrow (match f in F return (\lambda (_: +F).Prop) with [Appl \Rightarrow True | Cast \Rightarrow False])])])) I (THead +(Flat Cast) t2 t1) H5) in (False_ind (ex3 T (\lambda (t0: T).(pc3 c0 (THead +(Flat Cast) t0 t2) (THead (Flat Appl) w (THead (Bind Abst) u t)))) (\lambda +(_: T).(ty3 g c0 t1 t2)) (\lambda (t0: T).(ty3 g c0 t2 t0))) H6)))))))))))) +(\lambda (c0: C).(\lambda (t0: T).(\lambda (t3: T).(\lambda (H1: (ty3 g c0 t0 +t3)).(\lambda (H2: (((eq T t0 (THead (Flat Cast) t2 t1)) \to (ex3 T (\lambda +(t4: T).(pc3 c0 (THead (Flat Cast) t4 t2) t3)) (\lambda (_: T).(ty3 g c0 t1 +t2)) (\lambda (t4: T).(ty3 g c0 t2 t4)))))).(\lambda (t4: T).(\lambda (H3: (ty3 g c0 t3 t4)).(\lambda (H4: (((eq T t3 (THead (Flat Cast) t2 t1)) \to -(land (pc3 c0 t2 t4) (ty3 g c0 t1 t2))))).(\lambda (H5: (eq T (THead (Flat -Cast) t3 t0) (THead (Flat Cast) t2 t1))).(let H6 \def (f_equal T T (\lambda -(e: T).(match e in T return (\lambda (_: T).T) with [(TSort _) \Rightarrow t3 -| (TLRef _) \Rightarrow t3 | (THead _ t _) \Rightarrow t])) (THead (Flat -Cast) t3 t0) (THead (Flat Cast) t2 t1) H5) in ((let H7 \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 (Flat Cast) t3 t0) (THead (Flat Cast) t2 t1) H5) in (\lambda (H8: (eq -T t3 t2)).(let H9 \def (eq_ind T t3 (\lambda (t: T).((eq T t (THead (Flat -Cast) t2 t1)) \to (land (pc3 c0 t2 t4) (ty3 g c0 t1 t2)))) H4 t2 H8) in (let -H10 \def (eq_ind T t3 (\lambda (t: T).(ty3 g c0 t t4)) H3 t2 H8) in (let H11 -\def (eq_ind T t3 (\lambda (t: T).((eq T t0 (THead (Flat Cast) t2 t1)) \to -(land (pc3 c0 t2 t) (ty3 g c0 t1 t2)))) H2 t2 H8) in (let H12 \def (eq_ind T -t3 (\lambda (t: T).(ty3 g c0 t0 t)) H1 t2 H8) in (eq_ind_r T t2 (\lambda (t: -T).(land (pc3 c0 t2 t) (ty3 g c0 t1 t2))) (let H13 \def (eq_ind T t0 (\lambda -(t: T).((eq T t (THead (Flat Cast) t2 t1)) \to (land (pc3 c0 t2 t2) (ty3 g c0 -t1 t2)))) H11 t1 H7) in (let H14 \def (eq_ind T t0 (\lambda (t: T).(ty3 g c0 -t t2)) H12 t1 H7) in (conj (pc3 c0 t2 t2) (ty3 g c0 t1 t2) (pc3_refl c0 t2) -H14))) t3 H8))))))) H6))))))))))) c y x H0))) H)))))). +(ex3 T (\lambda (t5: T).(pc3 c0 (THead (Flat Cast) t5 t2) t4)) (\lambda (_: +T).(ty3 g c0 t1 t2)) (\lambda (t5: T).(ty3 g c0 t2 t5)))))).(\lambda (H5: (eq +T (THead (Flat Cast) t3 t0) (THead (Flat Cast) t2 t1))).(let H6 \def (f_equal +T T (\lambda (e: T).(match e in T return (\lambda (_: T).T) with [(TSort _) +\Rightarrow t3 | (TLRef _) \Rightarrow t3 | (THead _ t _) \Rightarrow t])) +(THead (Flat Cast) t3 t0) (THead (Flat Cast) t2 t1) H5) in ((let H7 \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 (Flat Cast) t3 t0) (THead (Flat Cast) t2 t1) H5) in +(\lambda (H8: (eq T t3 t2)).(let H9 \def (eq_ind T t3 (\lambda (t: T).((eq T +t (THead (Flat Cast) t2 t1)) \to (ex3 T (\lambda (t5: T).(pc3 c0 (THead (Flat +Cast) t5 t2) t4)) (\lambda (_: T).(ty3 g c0 t1 t2)) (\lambda (t5: T).(ty3 g +c0 t2 t5))))) H4 t2 H8) in (let H10 \def (eq_ind T t3 (\lambda (t: T).(ty3 g +c0 t t4)) H3 t2 H8) in (let H11 \def (eq_ind T t3 (\lambda (t: T).((eq T t0 +(THead (Flat Cast) t2 t1)) \to (ex3 T (\lambda (t5: T).(pc3 c0 (THead (Flat +Cast) t5 t2) t)) (\lambda (_: T).(ty3 g c0 t1 t2)) (\lambda (t5: T).(ty3 g c0 +t2 t5))))) H2 t2 H8) in (let H12 \def (eq_ind T t3 (\lambda (t: T).(ty3 g c0 +t0 t)) H1 t2 H8) in (eq_ind_r T t2 (\lambda (t: T).(ex3 T (\lambda (t5: +T).(pc3 c0 (THead (Flat Cast) t5 t2) (THead (Flat Cast) t4 t))) (\lambda (_: +T).(ty3 g c0 t1 t2)) (\lambda (t5: T).(ty3 g c0 t2 t5)))) (let H13 \def +(eq_ind T t0 (\lambda (t: T).((eq T t (THead (Flat Cast) t2 t1)) \to (ex3 T +(\lambda (t5: T).(pc3 c0 (THead (Flat Cast) t5 t2) t2)) (\lambda (_: T).(ty3 +g c0 t1 t2)) (\lambda (t5: T).(ty3 g c0 t2 t5))))) H11 t1 H7) in (let H14 +\def (eq_ind T t0 (\lambda (t: T).(ty3 g c0 t t2)) H12 t1 H7) in (ex3_intro T +(\lambda (t5: T).(pc3 c0 (THead (Flat Cast) t5 t2) (THead (Flat Cast) t4 +t2))) (\lambda (_: T).(ty3 g c0 t1 t2)) (\lambda (t5: T).(ty3 g c0 t2 t5)) t4 +(pc3_refl c0 (THead (Flat Cast) t4 t2)) H14 H10))) t3 H8))))))) H6))))))))))) +c y x H0))) H)))))). diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/pr3.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/pr3.ma index 99eb3bc22..bc53829ae 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/pr3.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/pr3.ma @@ -596,53 +596,60 @@ t3 t4) \to (ty3 g c2 t4 t0))))))).(\lambda (c2: C).(\lambda (H4: (wcpr0 c c2)).(\lambda (t4: T).(\lambda (H5: (pr0 (THead (Flat Cast) t3 t2) t4)).(let H6 \def (match H5 in pr0 return (\lambda (t5: T).(\lambda (t6: T).(\lambda (_: (pr0 t5 t6)).((eq T t5 (THead (Flat Cast) t3 t2)) \to ((eq T t6 t4) \to -(ty3 g c2 t4 t3)))))) with [(pr0_refl t5) \Rightarrow (\lambda (H6: (eq T t5 -(THead (Flat Cast) t3 t2))).(\lambda (H7: (eq T t5 t4)).(eq_ind T (THead -(Flat Cast) t3 t2) (\lambda (t6: T).((eq T t6 t4) \to (ty3 g c2 t4 t3))) -(\lambda (H8: (eq T (THead (Flat Cast) t3 t2) t4)).(eq_ind T (THead (Flat -Cast) t3 t2) (\lambda (t6: T).(ty3 g c2 t6 t3)) (ty3_cast g c2 t2 t3 (H1 c2 -H4 t2 (pr0_refl t2)) t0 (H3 c2 H4 t3 (pr0_refl t3))) t4 H8)) t5 (sym_eq T t5 -(THead (Flat Cast) t3 t2) H6) H7))) | (pr0_comp u1 u2 H6 t5 t6 H7 k) -\Rightarrow (\lambda (H8: (eq T (THead k u1 t5) (THead (Flat Cast) t3 -t2))).(\lambda (H9: (eq T (THead k u2 t6) t4)).((let H10 \def (f_equal T T -(\lambda (e: T).(match e in T return (\lambda (_: T).T) with [(TSort _) -\Rightarrow t5 | (TLRef _) \Rightarrow t5 | (THead _ _ t7) \Rightarrow t7])) -(THead k u1 t5) (THead (Flat Cast) t3 t2) H8) in ((let H11 \def (f_equal T T -(\lambda (e: T).(match e in T return (\lambda (_: T).T) with [(TSort _) -\Rightarrow u1 | (TLRef _) \Rightarrow u1 | (THead _ t7 _) \Rightarrow t7])) -(THead k u1 t5) (THead (Flat Cast) t3 t2) H8) in ((let H12 \def (f_equal T K -(\lambda (e: T).(match e in T return (\lambda (_: T).K) with [(TSort _) -\Rightarrow k | (TLRef _) \Rightarrow k | (THead k0 _ _) \Rightarrow k0])) -(THead k u1 t5) (THead (Flat Cast) t3 t2) H8) in (eq_ind K (Flat Cast) -(\lambda (k0: K).((eq T u1 t3) \to ((eq T t5 t2) \to ((eq T (THead k0 u2 t6) -t4) \to ((pr0 u1 u2) \to ((pr0 t5 t6) \to (ty3 g c2 t4 t3))))))) (\lambda -(H13: (eq T u1 t3)).(eq_ind T t3 (\lambda (t7: T).((eq T t5 t2) \to ((eq T -(THead (Flat Cast) u2 t6) t4) \to ((pr0 t7 u2) \to ((pr0 t5 t6) \to (ty3 g c2 -t4 t3)))))) (\lambda (H14: (eq T t5 t2)).(eq_ind T t2 (\lambda (t7: T).((eq T -(THead (Flat Cast) u2 t6) t4) \to ((pr0 t3 u2) \to ((pr0 t7 t6) \to (ty3 g c2 -t4 t3))))) (\lambda (H15: (eq T (THead (Flat Cast) u2 t6) t4)).(eq_ind T -(THead (Flat Cast) u2 t6) (\lambda (t7: T).((pr0 t3 u2) \to ((pr0 t2 t6) \to -(ty3 g c2 t7 t3)))) (\lambda (H16: (pr0 t3 u2)).(\lambda (H17: (pr0 t2 -t6)).(ty3_conv g c2 t3 t0 (H3 c2 H4 t3 (pr0_refl t3)) (THead (Flat Cast) u2 -t6) u2 (ty3_cast g c2 t6 u2 (ty3_conv g c2 u2 t0 (H3 c2 H4 u2 H16) t6 t3 (H1 -c2 H4 t6 H17) (pc3_pr2_r c2 t3 u2 (pr2_free c2 t3 u2 H16))) t0 (H3 c2 H4 u2 -H16)) (pc3_pr2_x c2 u2 t3 (pr2_free c2 t3 u2 H16))))) t4 H15)) t5 (sym_eq T -t5 t2 H14))) u1 (sym_eq T u1 t3 H13))) k (sym_eq K k (Flat Cast) H12))) H11)) -H10)) H9 H6 H7))) | (pr0_beta u v1 v2 H6 t5 t6 H7) \Rightarrow (\lambda (H8: -(eq T (THead (Flat Appl) v1 (THead (Bind Abst) u t5)) (THead (Flat Cast) t3 -t2))).(\lambda (H9: (eq T (THead (Bind Abbr) v2 t6) t4)).((let H10 \def -(eq_ind T (THead (Flat Appl) v1 (THead (Bind Abst) u t5)) (\lambda (e: -T).(match e in T return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow -False | (TLRef _) \Rightarrow False | (THead k _ _) \Rightarrow (match k in K -return (\lambda (_: K).Prop) with [(Bind _) \Rightarrow False | (Flat f) -\Rightarrow (match f in F return (\lambda (_: F).Prop) with [Appl \Rightarrow -True | Cast \Rightarrow False])])])) I (THead (Flat Cast) t3 t2) H8) in -(False_ind ((eq T (THead (Bind Abbr) v2 t6) t4) \to ((pr0 v1 v2) \to ((pr0 t5 -t6) \to (ty3 g c2 t4 t3)))) H10)) H9 H6 H7))) | (pr0_upsilon b H6 v1 v2 H7 u1 -u2 H8 t5 t6 H9) \Rightarrow (\lambda (H10: (eq T (THead (Flat Appl) v1 (THead -(Bind b) u1 t5)) (THead (Flat Cast) t3 t2))).(\lambda (H11: (eq T (THead -(Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t6)) t4)).((let H12 \def -(eq_ind T (THead (Flat Appl) v1 (THead (Bind b) u1 t5)) (\lambda (e: +(ty3 g c2 t4 (THead (Flat Cast) t0 t3))))))) with [(pr0_refl t5) \Rightarrow +(\lambda (H6: (eq T t5 (THead (Flat Cast) t3 t2))).(\lambda (H7: (eq T t5 +t4)).(eq_ind T (THead (Flat Cast) t3 t2) (\lambda (t6: T).((eq T t6 t4) \to +(ty3 g c2 t4 (THead (Flat Cast) t0 t3)))) (\lambda (H8: (eq T (THead (Flat +Cast) t3 t2) t4)).(eq_ind T (THead (Flat Cast) t3 t2) (\lambda (t6: T).(ty3 g +c2 t6 (THead (Flat Cast) t0 t3))) (ty3_cast g c2 t2 t3 (H1 c2 H4 t2 (pr0_refl +t2)) t0 (H3 c2 H4 t3 (pr0_refl t3))) t4 H8)) t5 (sym_eq T t5 (THead (Flat +Cast) t3 t2) H6) H7))) | (pr0_comp u1 u2 H6 t5 t6 H7 k) \Rightarrow (\lambda +(H8: (eq T (THead k u1 t5) (THead (Flat Cast) t3 t2))).(\lambda (H9: (eq T +(THead k u2 t6) t4)).((let H10 \def (f_equal T T (\lambda (e: T).(match e in +T return (\lambda (_: T).T) with [(TSort _) \Rightarrow t5 | (TLRef _) +\Rightarrow t5 | (THead _ _ t7) \Rightarrow t7])) (THead k u1 t5) (THead +(Flat Cast) t3 t2) H8) in ((let H11 \def (f_equal T T (\lambda (e: T).(match +e in T return (\lambda (_: T).T) with [(TSort _) \Rightarrow u1 | (TLRef _) +\Rightarrow u1 | (THead _ t7 _) \Rightarrow t7])) (THead k u1 t5) (THead +(Flat Cast) t3 t2) H8) in ((let H12 \def (f_equal T K (\lambda (e: T).(match +e in T return (\lambda (_: T).K) with [(TSort _) \Rightarrow k | (TLRef _) +\Rightarrow k | (THead k0 _ _) \Rightarrow k0])) (THead k u1 t5) (THead (Flat +Cast) t3 t2) H8) in (eq_ind K (Flat Cast) (\lambda (k0: K).((eq T u1 t3) \to +((eq T t5 t2) \to ((eq T (THead k0 u2 t6) t4) \to ((pr0 u1 u2) \to ((pr0 t5 +t6) \to (ty3 g c2 t4 (THead (Flat Cast) t0 t3)))))))) (\lambda (H13: (eq T u1 +t3)).(eq_ind T t3 (\lambda (t7: T).((eq T t5 t2) \to ((eq T (THead (Flat +Cast) u2 t6) t4) \to ((pr0 t7 u2) \to ((pr0 t5 t6) \to (ty3 g c2 t4 (THead +(Flat Cast) t0 t3))))))) (\lambda (H14: (eq T t5 t2)).(eq_ind T t2 (\lambda +(t7: T).((eq T (THead (Flat Cast) u2 t6) t4) \to ((pr0 t3 u2) \to ((pr0 t7 +t6) \to (ty3 g c2 t4 (THead (Flat Cast) t0 t3)))))) (\lambda (H15: (eq T +(THead (Flat Cast) u2 t6) t4)).(eq_ind T (THead (Flat Cast) u2 t6) (\lambda +(t7: T).((pr0 t3 u2) \to ((pr0 t2 t6) \to (ty3 g c2 t7 (THead (Flat Cast) t0 +t3))))) (\lambda (H16: (pr0 t3 u2)).(\lambda (H17: (pr0 t2 t6)).(ex_ind T +(\lambda (t7: T).(ty3 g c2 t0 t7)) (ty3 g c2 (THead (Flat Cast) u2 t6) (THead +(Flat Cast) t0 t3)) (\lambda (x: T).(\lambda (H18: (ty3 g c2 t0 x)).(ty3_conv +g c2 (THead (Flat Cast) t0 t3) (THead (Flat Cast) x t0) (ty3_cast g c2 t3 t0 +(H3 c2 H4 t3 (pr0_refl t3)) x H18) (THead (Flat Cast) u2 t6) (THead (Flat +Cast) t0 u2) (ty3_cast g c2 t6 u2 (ty3_conv g c2 u2 t0 (H3 c2 H4 u2 H16) t6 +t3 (H1 c2 H4 t6 H17) (pc3_pr2_r c2 t3 u2 (pr2_free c2 t3 u2 H16))) t0 (H3 c2 +H4 u2 H16)) (pc3_pr2_x c2 (THead (Flat Cast) t0 u2) (THead (Flat Cast) t0 t3) +(pr2_thin_dx c2 t3 u2 (pr2_free c2 t3 u2 H16) t0 Cast))))) (ty3_correct g c2 +t3 t0 (H3 c2 H4 t3 (pr0_refl t3)))))) t4 H15)) t5 (sym_eq T t5 t2 H14))) u1 +(sym_eq T u1 t3 H13))) k (sym_eq K k (Flat Cast) H12))) H11)) H10)) H9 H6 +H7))) | (pr0_beta u v1 v2 H6 t5 t6 H7) \Rightarrow (\lambda (H8: (eq T (THead +(Flat Appl) v1 (THead (Bind Abst) u t5)) (THead (Flat Cast) t3 t2))).(\lambda +(H9: (eq T (THead (Bind Abbr) v2 t6) t4)).((let H10 \def (eq_ind T (THead +(Flat Appl) v1 (THead (Bind Abst) u t5)) (\lambda (e: T).(match e in T return +(\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef _) +\Rightarrow False | (THead k _ _) \Rightarrow (match k in K return (\lambda +(_: K).Prop) with [(Bind _) \Rightarrow False | (Flat f) \Rightarrow (match f +in F return (\lambda (_: F).Prop) with [Appl \Rightarrow True | Cast +\Rightarrow False])])])) I (THead (Flat Cast) t3 t2) H8) in (False_ind ((eq T +(THead (Bind Abbr) v2 t6) t4) \to ((pr0 v1 v2) \to ((pr0 t5 t6) \to (ty3 g c2 +t4 (THead (Flat Cast) t0 t3))))) H10)) H9 H6 H7))) | (pr0_upsilon b H6 v1 v2 +H7 u1 u2 H8 t5 t6 H9) \Rightarrow (\lambda (H10: (eq T (THead (Flat Appl) v1 +(THead (Bind b) u1 t5)) (THead (Flat Cast) t3 t2))).(\lambda (H11: (eq T +(THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t6)) t4)).((let H12 +\def (eq_ind T (THead (Flat Appl) v1 (THead (Bind b) u1 t5)) (\lambda (e: T).(match e in T return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow False | (THead k _ _) \Rightarrow (match k in K return (\lambda (_: K).Prop) with [(Bind _) \Rightarrow False | (Flat f) @@ -650,40 +657,47 @@ return (\lambda (_: K).Prop) with [(Bind _) \Rightarrow False | (Flat f) True | Cast \Rightarrow False])])])) I (THead (Flat Cast) t3 t2) H10) in (False_ind ((eq T (THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t6)) t4) \to ((not (eq B b Abst)) \to ((pr0 v1 v2) \to ((pr0 u1 u2) \to ((pr0 -t5 t6) \to (ty3 g c2 t4 t3)))))) H12)) H11 H6 H7 H8 H9))) | (pr0_delta u1 u2 -H6 t5 t6 H7 w H8) \Rightarrow (\lambda (H9: (eq T (THead (Bind Abbr) u1 t5) -(THead (Flat Cast) t3 t2))).(\lambda (H10: (eq T (THead (Bind Abbr) u2 w) -t4)).((let H11 \def (eq_ind T (THead (Bind Abbr) u1 t5) (\lambda (e: -T).(match e in T return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow -False | (TLRef _) \Rightarrow False | (THead k _ _) \Rightarrow (match k in K -return (\lambda (_: K).Prop) with [(Bind _) \Rightarrow True | (Flat _) -\Rightarrow False])])) I (THead (Flat Cast) t3 t2) H9) in (False_ind ((eq T -(THead (Bind Abbr) u2 w) t4) \to ((pr0 u1 u2) \to ((pr0 t5 t6) \to ((subst0 O -u2 t6 w) \to (ty3 g c2 t4 t3))))) H11)) H10 H6 H7 H8))) | (pr0_zeta b H6 t5 -t6 H7 u) \Rightarrow (\lambda (H8: (eq T (THead (Bind b) u (lift (S O) O t5)) -(THead (Flat Cast) t3 t2))).(\lambda (H9: (eq T t6 t4)).((let H10 \def -(eq_ind T (THead (Bind b) u (lift (S O) O t5)) (\lambda (e: T).(match e in T -return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef _) -\Rightarrow False | (THead k _ _) \Rightarrow (match k in K return (\lambda -(_: K).Prop) with [(Bind _) \Rightarrow True | (Flat _) \Rightarrow -False])])) I (THead (Flat Cast) t3 t2) H8) in (False_ind ((eq T t6 t4) \to -((not (eq B b Abst)) \to ((pr0 t5 t6) \to (ty3 g c2 t4 t3)))) H10)) H9 H6 -H7))) | (pr0_epsilon t5 t6 H6 u) \Rightarrow (\lambda (H7: (eq T (THead (Flat -Cast) u t5) (THead (Flat Cast) t3 t2))).(\lambda (H8: (eq T t6 t4)).((let H9 -\def (f_equal T T (\lambda (e: T).(match e in T return (\lambda (_: T).T) -with [(TSort _) \Rightarrow t5 | (TLRef _) \Rightarrow t5 | (THead _ _ t7) +t5 t6) \to (ty3 g c2 t4 (THead (Flat Cast) t0 t3))))))) H12)) H11 H6 H7 H8 +H9))) | (pr0_delta u1 u2 H6 t5 t6 H7 w H8) \Rightarrow (\lambda (H9: (eq T +(THead (Bind Abbr) u1 t5) (THead (Flat Cast) t3 t2))).(\lambda (H10: (eq T +(THead (Bind Abbr) u2 w) t4)).((let H11 \def (eq_ind T (THead (Bind Abbr) u1 +t5) (\lambda (e: T).(match e in T return (\lambda (_: T).Prop) with [(TSort +_) \Rightarrow False | (TLRef _) \Rightarrow False | (THead k _ _) +\Rightarrow (match k in K return (\lambda (_: K).Prop) with [(Bind _) +\Rightarrow True | (Flat _) \Rightarrow False])])) I (THead (Flat Cast) t3 +t2) H9) in (False_ind ((eq T (THead (Bind Abbr) u2 w) t4) \to ((pr0 u1 u2) +\to ((pr0 t5 t6) \to ((subst0 O u2 t6 w) \to (ty3 g c2 t4 (THead (Flat Cast) +t0 t3)))))) H11)) H10 H6 H7 H8))) | (pr0_zeta b H6 t5 t6 H7 u) \Rightarrow +(\lambda (H8: (eq T (THead (Bind b) u (lift (S O) O t5)) (THead (Flat Cast) +t3 t2))).(\lambda (H9: (eq T t6 t4)).((let H10 \def (eq_ind T (THead (Bind b) +u (lift (S O) O t5)) (\lambda (e: T).(match e in T return (\lambda (_: +T).Prop) with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow False | +(THead k _ _) \Rightarrow (match k in K return (\lambda (_: K).Prop) with +[(Bind _) \Rightarrow True | (Flat _) \Rightarrow False])])) I (THead (Flat +Cast) t3 t2) H8) in (False_ind ((eq T t6 t4) \to ((not (eq B b Abst)) \to +((pr0 t5 t6) \to (ty3 g c2 t4 (THead (Flat Cast) t0 t3))))) H10)) H9 H6 H7))) +| (pr0_epsilon t5 t6 H6 u) \Rightarrow (\lambda (H7: (eq T (THead (Flat Cast) +u t5) (THead (Flat Cast) t3 t2))).(\lambda (H8: (eq T t6 t4)).((let H9 \def +(f_equal T T (\lambda (e: T).(match e in T return (\lambda (_: T).T) with +[(TSort _) \Rightarrow t5 | (TLRef _) \Rightarrow t5 | (THead _ _ t7) \Rightarrow t7])) (THead (Flat Cast) u t5) (THead (Flat Cast) t3 t2) H7) in ((let H10 \def (f_equal T T (\lambda (e: T).(match e in T return (\lambda (_: T).T) with [(TSort _) \Rightarrow u | (TLRef _) \Rightarrow u | (THead _ t7 _) \Rightarrow t7])) (THead (Flat Cast) u t5) (THead (Flat Cast) t3 t2) H7) in (eq_ind T t3 (\lambda (_: T).((eq T t5 t2) \to ((eq T t6 t4) \to ((pr0 t5 -t6) \to (ty3 g c2 t4 t3))))) (\lambda (H11: (eq T t5 t2)).(eq_ind T t2 -(\lambda (t7: T).((eq T t6 t4) \to ((pr0 t7 t6) \to (ty3 g c2 t4 t3)))) -(\lambda (H12: (eq T t6 t4)).(eq_ind T t4 (\lambda (t7: T).((pr0 t2 t7) \to -(ty3 g c2 t4 t3))) (\lambda (H13: (pr0 t2 t4)).(H1 c2 H4 t4 H13)) t6 (sym_eq -T t6 t4 H12))) t5 (sym_eq T t5 t2 H11))) u (sym_eq T u t3 H10))) H9)) H8 -H6)))]) in (H6 (refl_equal T (THead (Flat Cast) t3 t2)) (refl_equal T -t4))))))))))))))) c1 t1 t H))))). +t6) \to (ty3 g c2 t4 (THead (Flat Cast) t0 t3)))))) (\lambda (H11: (eq T t5 +t2)).(eq_ind T t2 (\lambda (t7: T).((eq T t6 t4) \to ((pr0 t7 t6) \to (ty3 g +c2 t4 (THead (Flat Cast) t0 t3))))) (\lambda (H12: (eq T t6 t4)).(eq_ind T t4 +(\lambda (t7: T).((pr0 t2 t7) \to (ty3 g c2 t4 (THead (Flat Cast) t0 t3)))) +(\lambda (H13: (pr0 t2 t4)).(ex_ind T (\lambda (t7: T).(ty3 g c2 t0 t7)) (ty3 +g c2 t4 (THead (Flat Cast) t0 t3)) (\lambda (x: T).(\lambda (H14: (ty3 g c2 +t0 x)).(ty3_conv g c2 (THead (Flat Cast) t0 t3) (THead (Flat Cast) x t0) +(ty3_cast g c2 t3 t0 (H3 c2 H4 t3 (pr0_refl t3)) x H14) t4 t3 (H1 c2 H4 t4 +H13) (pc3_pr2_x c2 t3 (THead (Flat Cast) t0 t3) (pr2_free c2 (THead (Flat +Cast) t0 t3) t3 (pr0_epsilon t3 t3 (pr0_refl t3) t0)))))) (ty3_correct g c2 +t3 t0 (H3 c2 H4 t3 (pr0_refl t3))))) t6 (sym_eq T t6 t4 H12))) t5 (sym_eq T +t5 t2 H11))) u (sym_eq T u t3 H10))) H9)) H8 H6)))]) in (H6 (refl_equal T +(THead (Flat Cast) t3 t2)) (refl_equal T t4))))))))))))))) c1 t1 t H))))). theorem ty3_sred_pr1: \forall (c: C).(\forall (t1: T).(\forall (t2: T).((pr1 t1 t2) \to (\forall diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/pr3_props.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/pr3_props.ma index 6cf0c095a..3a17df985 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/pr3_props.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/pr3_props.ma @@ -414,40 +414,45 @@ x0 t4)))))))))).(\lambda (x0: T).(\lambda (x1: nat).(\lambda (H5: (eq T (drop h x1 c0 e)).(ex3_2_ind T T (\lambda (y0: T).(\lambda (z: T).(eq T x0 (THead (Flat Cast) y0 z)))) (\lambda (y0: T).(\lambda (_: T).(eq T t3 (lift h x1 y0)))) (\lambda (_: T).(\lambda (z: T).(eq T t2 (lift h x1 z)))) (ex2 T -(\lambda (t4: T).(pc3 c0 (lift h x1 t4) t3)) (\lambda (t4: T).(ty3 g e x0 -t4))) (\lambda (x2: T).(\lambda (x3: T).(\lambda (H7: (eq T x0 (THead (Flat -Cast) x2 x3))).(\lambda (H8: (eq T t3 (lift h x1 x2))).(\lambda (H9: (eq T t2 -(lift h x1 x3))).(eq_ind_r T (THead (Flat Cast) x2 x3) (\lambda (t: T).(ex2 T -(\lambda (t4: T).(pc3 c0 (lift h x1 t4) t3)) (\lambda (t4: T).(ty3 g e t -t4)))) (let H10 \def (eq_ind T t3 (\lambda (t: T).(\forall (x4: T).(\forall -(x5: nat).((eq T t (lift h x5 x4)) \to (\forall (e0: C).((drop h x5 c0 e0) -\to (ex2 T (\lambda (t4: T).(pc3 c0 (lift h x5 t4) t0)) (\lambda (t4: T).(ty3 -g e0 x4 t4))))))))) H4 (lift h x1 x2) H8) in (let H11 \def (eq_ind T t3 -(\lambda (t: T).(ty3 g c0 t t0)) H3 (lift h x1 x2) H8) in (let H12 \def -(eq_ind T t3 (\lambda (t: T).(\forall (x4: T).(\forall (x5: nat).((eq T t2 -(lift h x5 x4)) \to (\forall (e0: C).((drop h x5 c0 e0) \to (ex2 T (\lambda -(t4: T).(pc3 c0 (lift h x5 t4) t)) (\lambda (t4: T).(ty3 g e0 x4 t4))))))))) -H2 (lift h x1 x2) H8) in (let H13 \def (eq_ind T t3 (\lambda (t: T).(ty3 g c0 -t2 t)) H1 (lift h x1 x2) H8) in (eq_ind_r T (lift h x1 x2) (\lambda (t: -T).(ex2 T (\lambda (t4: T).(pc3 c0 (lift h x1 t4) t)) (\lambda (t4: T).(ty3 g -e (THead (Flat Cast) x2 x3) t4)))) (let H14 \def (eq_ind T t2 (\lambda (t: -T).(ty3 g c0 t (lift h x1 x2))) H13 (lift h x1 x3) H9) in (let H15 \def -(eq_ind T t2 (\lambda (t: T).(\forall (x4: T).(\forall (x5: nat).((eq T t -(lift h x5 x4)) \to (\forall (e0: C).((drop h x5 c0 e0) \to (ex2 T (\lambda -(t4: T).(pc3 c0 (lift h x5 t4) (lift h x1 x2))) (\lambda (t4: T).(ty3 g e0 x4 -t4))))))))) H12 (lift h x1 x3) H9) in (let H16 \def (H15 x3 x1 (refl_equal T -(lift h x1 x3)) e H6) in (ex2_ind T (\lambda (t4: T).(pc3 c0 (lift h x1 t4) -(lift h x1 x2))) (\lambda (t4: T).(ty3 g e x3 t4)) (ex2 T (\lambda (t4: -T).(pc3 c0 (lift h x1 t4) (lift h x1 x2))) (\lambda (t4: T).(ty3 g e (THead +(\lambda (t4: T).(pc3 c0 (lift h x1 t4) (THead (Flat Cast) t0 t3))) (\lambda +(t4: T).(ty3 g e x0 t4))) (\lambda (x2: T).(\lambda (x3: T).(\lambda (H7: (eq +T x0 (THead (Flat Cast) x2 x3))).(\lambda (H8: (eq T t3 (lift h x1 +x2))).(\lambda (H9: (eq T t2 (lift h x1 x3))).(eq_ind_r T (THead (Flat Cast) +x2 x3) (\lambda (t: T).(ex2 T (\lambda (t4: T).(pc3 c0 (lift h x1 t4) (THead +(Flat Cast) t0 t3))) (\lambda (t4: T).(ty3 g e t t4)))) (let H10 \def (eq_ind +T t3 (\lambda (t: T).(\forall (x4: T).(\forall (x5: nat).((eq T t (lift h x5 +x4)) \to (\forall (e0: C).((drop h x5 c0 e0) \to (ex2 T (\lambda (t4: T).(pc3 +c0 (lift h x5 t4) t0)) (\lambda (t4: T).(ty3 g e0 x4 t4))))))))) H4 (lift h +x1 x2) H8) in (let H11 \def (eq_ind T t3 (\lambda (t: T).(ty3 g c0 t t0)) H3 +(lift h x1 x2) H8) in (let H12 \def (eq_ind T t3 (\lambda (t: T).(\forall +(x4: T).(\forall (x5: nat).((eq T t2 (lift h x5 x4)) \to (\forall (e0: +C).((drop h x5 c0 e0) \to (ex2 T (\lambda (t4: T).(pc3 c0 (lift h x5 t4) t)) +(\lambda (t4: T).(ty3 g e0 x4 t4))))))))) H2 (lift h x1 x2) H8) in (let H13 +\def (eq_ind T t3 (\lambda (t: T).(ty3 g c0 t2 t)) H1 (lift h x1 x2) H8) in +(eq_ind_r T (lift h x1 x2) (\lambda (t: T).(ex2 T (\lambda (t4: T).(pc3 c0 +(lift h x1 t4) (THead (Flat Cast) t0 t))) (\lambda (t4: T).(ty3 g e (THead +(Flat Cast) x2 x3) t4)))) (let H14 \def (eq_ind T t2 (\lambda (t: T).(ty3 g +c0 t (lift h x1 x2))) H13 (lift h x1 x3) H9) in (let H15 \def (eq_ind T t2 +(\lambda (t: T).(\forall (x4: T).(\forall (x5: nat).((eq T t (lift h x5 x4)) +\to (\forall (e0: C).((drop h x5 c0 e0) \to (ex2 T (\lambda (t4: T).(pc3 c0 +(lift h x5 t4) (lift h x1 x2))) (\lambda (t4: T).(ty3 g e0 x4 t4))))))))) H12 +(lift h x1 x3) H9) in (let H16 \def (H15 x3 x1 (refl_equal T (lift h x1 x3)) +e H6) in (ex2_ind T (\lambda (t4: T).(pc3 c0 (lift h x1 t4) (lift h x1 x2))) +(\lambda (t4: T).(ty3 g e x3 t4)) (ex2 T (\lambda (t4: T).(pc3 c0 (lift h x1 +t4) (THead (Flat Cast) t0 (lift h x1 x2)))) (\lambda (t4: T).(ty3 g e (THead (Flat Cast) x2 x3) t4))) (\lambda (x4: T).(\lambda (H17: (pc3 c0 (lift h x1 x4) (lift h x1 x2))).(\lambda (H18: (ty3 g e x3 x4)).(let H19 \def (H10 x2 x1 (refl_equal T (lift h x1 x2)) e H6) in (ex2_ind T (\lambda (t4: T).(pc3 c0 (lift h x1 t4) t0)) (\lambda (t4: T).(ty3 g e x2 t4)) (ex2 T (\lambda (t4: -T).(pc3 c0 (lift h x1 t4) (lift h x1 x2))) (\lambda (t4: T).(ty3 g e (THead -(Flat Cast) x2 x3) t4))) (\lambda (x5: T).(\lambda (_: (pc3 c0 (lift h x1 x5) -t0)).(\lambda (H21: (ty3 g e x2 x5)).(ex_intro2 T (\lambda (t4: T).(pc3 c0 -(lift h x1 t4) (lift h x1 x2))) (\lambda (t4: T).(ty3 g e (THead (Flat Cast) -x2 x3) t4)) x2 (pc3_refl c0 (lift h x1 x2)) (ty3_cast g e x3 x2 (ty3_conv g e +T).(pc3 c0 (lift h x1 t4) (THead (Flat Cast) t0 (lift h x1 x2)))) (\lambda +(t4: T).(ty3 g e (THead (Flat Cast) x2 x3) t4))) (\lambda (x5: T).(\lambda +(H20: (pc3 c0 (lift h x1 x5) t0)).(\lambda (H21: (ty3 g e x2 x5)).(ex_intro2 +T (\lambda (t4: T).(pc3 c0 (lift h x1 t4) (THead (Flat Cast) t0 (lift h x1 +x2)))) (\lambda (t4: T).(ty3 g e (THead (Flat Cast) x2 x3) t4)) (THead (Flat +Cast) x5 x2) (eq_ind_r T (THead (Flat Cast) (lift h x1 x5) (lift h x1 x2)) +(\lambda (t: T).(pc3 c0 t (THead (Flat Cast) t0 (lift h x1 x2)))) (pc3_head_1 +c0 (lift h x1 x5) t0 H20 (Flat Cast) (lift h x1 x2)) (lift h x1 (THead (Flat +Cast) x5 x2)) (lift_flat Cast x5 x2 h x1)) (ty3_cast g e x3 x2 (ty3_conv g e x2 x5 H21 x3 x4 H18 (pc3_gen_lift c0 x4 x2 h x1 H17 e H6)) x5 H21))))) H19))))) H16)))) t3 H8))))) x0 H7)))))) (lift_gen_flat Cast t3 t2 x0 h x1 H5))))))))))))))) c y x H0))))) H))))))). diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/props.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/props.ma index 4fe0d6385..d69a6dc4a 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/props.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/props.ma @@ -179,10 +179,14 @@ C).(\lambda (t0: T).(\lambda (t3: T).(\lambda (_: (ty3 g c t0 t3)).(\lambda nat).(\forall (h: nat).((drop h d c0 c) \to (ty3 g c0 (lift h d t3) (lift h d t4)))))))).(\lambda (c0: C).(\lambda (d: nat).(\lambda (h: nat).(\lambda (H4: (drop h d c0 c)).(eq_ind_r T (THead (Flat Cast) (lift h d t3) (lift h (s -(Flat Cast) d) t0)) (\lambda (t: T).(ty3 g c0 t (lift h d t3))) (ty3_cast g -c0 (lift h (s (Flat Cast) d) t0) (lift h d t3) (H1 c0 d h H4) (lift h d t4) -(H3 c0 d h H4)) (lift h d (THead (Flat Cast) t3 t0)) (lift_head (Flat Cast) -t3 t0 h d)))))))))))))) e t1 t2 H))))). +(Flat Cast) d) t0)) (\lambda (t: T).(ty3 g c0 t (lift h d (THead (Flat Cast) +t4 t3)))) (eq_ind_r T (THead (Flat Cast) (lift h d t4) (lift h (s (Flat Cast) +d) t3)) (\lambda (t: T).(ty3 g c0 (THead (Flat Cast) (lift h d t3) (lift h (s +(Flat Cast) d) t0)) t)) (ty3_cast g c0 (lift h (s (Flat Cast) d) t0) (lift h +(s (Flat Cast) d) t3) (H1 c0 (s (Flat Cast) d) h H4) (lift h d t4) (H3 c0 d h +H4)) (lift h d (THead (Flat Cast) t4 t3)) (lift_head (Flat Cast) t4 t3 h d)) +(lift h d (THead (Flat Cast) t3 t0)) (lift_head (Flat Cast) t3 t0 h +d)))))))))))))) e t1 t2 H))))). theorem ty3_correct: \forall (g: G).(\forall (c: C).(\forall (t1: T).(\forall (t2: T).((ty3 g c @@ -244,10 +248,14 @@ T).(ty3 g c0 (THead (Flat Appl) w (THead (Bind Abst) u t)) t0)) (THead (Flat Appl) w (THead (Bind Abst) u x1)) (ty3_appl g c0 w u H0 (THead (Bind Abst) u t) x1 (ty3_bind g c0 u x2 H9 Abst t x1 H10 x3 H11)))))))))) (ty3_gen_bind g Abst c0 u t x0 H7)))) H6)))) H4))))))))))) (\lambda (c0: C).(\lambda (t0: -T).(\lambda (t3: T).(\lambda (_: (ty3 g c0 t0 t3)).(\lambda (H1: (ex T -(\lambda (t: T).(ty3 g c0 t3 t)))).(\lambda (t4: T).(\lambda (_: (ty3 g c0 t3 -t4)).(\lambda (_: (ex T (\lambda (t: T).(ty3 g c0 t4 t)))).H1)))))))) c t1 t2 -H))))). +T).(\lambda (t3: T).(\lambda (_: (ty3 g c0 t0 t3)).(\lambda (_: (ex T +(\lambda (t: T).(ty3 g c0 t3 t)))).(\lambda (t4: T).(\lambda (H2: (ty3 g c0 +t3 t4)).(\lambda (H3: (ex T (\lambda (t: T).(ty3 g c0 t4 t)))).(let H4 \def +H3 in (ex_ind T (\lambda (t: T).(ty3 g c0 t4 t)) (ex T (\lambda (t: T).(ty3 g +c0 (THead (Flat Cast) t4 t3) t))) (\lambda (x: T).(\lambda (H5: (ty3 g c0 t4 +x)).(ex_intro T (\lambda (t: T).(ty3 g c0 (THead (Flat Cast) t4 t3) t)) +(THead (Flat Cast) x t4) (ty3_cast g c0 t3 t4 H2 x H5)))) H4)))))))))) c t1 +t2 H))))). theorem ty3_unique: \forall (g: G).(\forall (c: C).(\forall (u: T).(\forall (t1: T).((ty3 g c u @@ -416,11 +424,15 @@ x1) (H3 (THead (Bind Abst) x0 x1) H6) w Appl) t2 H5)))))) (ty3_gen_appl g c0 w v t2 H4))))))))))))) (\lambda (c0: C).(\lambda (t0: T).(\lambda (t2: T).(\lambda (_: (ty3 g c0 t0 t2)).(\lambda (_: ((\forall (t3: T).((ty3 g c0 t0 t3) \to (pc3 c0 t2 t3))))).(\lambda (t3: T).(\lambda (_: (ty3 g c0 t2 -t3)).(\lambda (_: ((\forall (t4: T).((ty3 g c0 t2 t4) \to (pc3 c0 t3 +t3)).(\lambda (H3: ((\forall (t4: T).((ty3 g c0 t2 t4) \to (pc3 c0 t3 t4))))).(\lambda (t4: T).(\lambda (H4: (ty3 g c0 (THead (Flat Cast) t2 t0) -t4)).(and_ind (pc3 c0 t2 t4) (ty3 g c0 t0 t2) (pc3 c0 t2 t4) (\lambda (H5: -(pc3 c0 t2 t4)).(\lambda (_: (ty3 g c0 t0 t2)).H5)) (ty3_gen_cast g c0 t0 t2 -t4 H4)))))))))))) c u t1 H))))). +t4)).(ex3_ind T (\lambda (t5: T).(pc3 c0 (THead (Flat Cast) t5 t2) t4)) +(\lambda (_: T).(ty3 g c0 t0 t2)) (\lambda (t5: T).(ty3 g c0 t2 t5)) (pc3 c0 +(THead (Flat Cast) t3 t2) t4) (\lambda (x0: T).(\lambda (H5: (pc3 c0 (THead +(Flat Cast) x0 t2) t4)).(\lambda (_: (ty3 g c0 t0 t2)).(\lambda (H7: (ty3 g +c0 t2 x0)).(pc3_t (THead (Flat Cast) x0 t2) c0 (THead (Flat Cast) t3 t2) +(pc3_head_1 c0 t3 x0 (H3 x0 H7) (Flat Cast) t2) t4 H5))))) (ty3_gen_cast g c0 +t0 t2 t4 H4)))))))))))) c u t1 H))))). theorem ty3_gen_abst_abst: \forall (g: G).(\forall (c: C).(\forall (u: T).(\forall (t1: T).(\forall @@ -469,6 +481,7 @@ v) \to (ex T (\lambda (u: T).(ty3 g c (THead (Flat Cast) v t) u))))))) \lambda (g: G).(\lambda (c: C).(\lambda (t: T).(\lambda (v: T).(\lambda (H: (ty3 g c t v)).(ex_ind T (\lambda (t0: T).(ty3 g c v t0)) (ex T (\lambda (u: T).(ty3 g c (THead (Flat Cast) v t) u))) (\lambda (x: T).(\lambda (H0: (ty3 g -c v x)).(ex_intro T (\lambda (u: T).(ty3 g c (THead (Flat Cast) v t) u)) v -(ty3_cast g c t v H x H0)))) (ty3_correct g c t v H)))))). +c v x)).(ex_intro T (\lambda (u: T).(ty3 g c (THead (Flat Cast) v t) u)) +(THead (Flat Cast) x v) (ty3_cast g c t v H x H0)))) (ty3_correct g c t v +H)))))). diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/subst1.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/subst1.ma index 7a91362cc..60e08dbe1 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/subst1.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/subst1.ma @@ -554,28 +554,34 @@ in (ex3_2_ind T T (\lambda (y1: T).(\lambda (_: T).(subst1 d u t4 (lift (S O) d y1)))) (\lambda (_: T).(\lambda (y2: T).(subst1 d u t0 (lift (S O) d y2)))) (\lambda (y1: T).(\lambda (y2: T).(ty3 g a y1 y2))) (ex3_2 T T (\lambda (y1: T).(\lambda (_: T).(subst1 d u (THead (Flat Cast) t4 t3) (lift (S O) d y1)))) -(\lambda (_: T).(\lambda (y2: T).(subst1 d u t4 (lift (S O) d y2)))) (\lambda -(y1: T).(\lambda (y2: T).(ty3 g a y1 y2)))) (\lambda (x0: T).(\lambda (x1: -T).(\lambda (H8: (subst1 d u t4 (lift (S O) d x0))).(\lambda (_: (subst1 d u -t0 (lift (S O) d x1))).(\lambda (H10: (ty3 g a x0 x1)).(let H11 \def (H1 e u -d H4 a0 H5 a H6) in (ex3_2_ind T T (\lambda (y1: T).(\lambda (_: T).(subst1 d -u t3 (lift (S O) d y1)))) (\lambda (_: T).(\lambda (y2: T).(subst1 d u t4 -(lift (S O) d y2)))) (\lambda (y1: T).(\lambda (y2: T).(ty3 g a y1 y2))) -(ex3_2 T T (\lambda (y1: T).(\lambda (_: T).(subst1 d u (THead (Flat Cast) t4 -t3) (lift (S O) d y1)))) (\lambda (_: T).(\lambda (y2: T).(subst1 d u t4 -(lift (S O) d y2)))) (\lambda (y1: T).(\lambda (y2: T).(ty3 g a y1 y2)))) -(\lambda (x2: T).(\lambda (x3: T).(\lambda (H12: (subst1 d u t3 (lift (S O) d +(\lambda (_: T).(\lambda (y2: T).(subst1 d u (THead (Flat Cast) t0 t4) (lift +(S O) d y2)))) (\lambda (y1: T).(\lambda (y2: T).(ty3 g a y1 y2)))) (\lambda +(x0: T).(\lambda (x1: T).(\lambda (H8: (subst1 d u t4 (lift (S O) d +x0))).(\lambda (H9: (subst1 d u t0 (lift (S O) d x1))).(\lambda (H10: (ty3 g +a x0 x1)).(let H11 \def (H1 e u d H4 a0 H5 a H6) in (ex3_2_ind T T (\lambda +(y1: T).(\lambda (_: T).(subst1 d u t3 (lift (S O) d y1)))) (\lambda (_: +T).(\lambda (y2: T).(subst1 d u t4 (lift (S O) d y2)))) (\lambda (y1: +T).(\lambda (y2: T).(ty3 g a y1 y2))) (ex3_2 T T (\lambda (y1: T).(\lambda +(_: T).(subst1 d u (THead (Flat Cast) t4 t3) (lift (S O) d y1)))) (\lambda +(_: T).(\lambda (y2: T).(subst1 d u (THead (Flat Cast) t0 t4) (lift (S O) d +y2)))) (\lambda (y1: T).(\lambda (y2: T).(ty3 g a y1 y2)))) (\lambda (x2: +T).(\lambda (x3: T).(\lambda (H12: (subst1 d u t3 (lift (S O) d x2))).(\lambda (H13: (subst1 d u t4 (lift (S O) d x3))).(\lambda (H14: (ty3 g a x2 x3)).(let H15 \def (eq_ind T x3 (\lambda (t: T).(ty3 g a x2 t)) H14 x0 (subst1_confluence_lift t4 x3 u d H13 x0 H8)) in (ex3_2_intro T T (\lambda (y1: T).(\lambda (_: T).(subst1 d u (THead (Flat Cast) t4 t3) (lift (S O) d -y1)))) (\lambda (_: T).(\lambda (y2: T).(subst1 d u t4 (lift (S O) d y2)))) -(\lambda (y1: T).(\lambda (y2: T).(ty3 g a y1 y2))) (THead (Flat Cast) x0 x2) -x0 (eq_ind_r T (THead (Flat Cast) (lift (S O) d x0) (lift (S O) d x2)) -(\lambda (t: T).(subst1 d u (THead (Flat Cast) t4 t3) t)) (subst1_head u t4 -(lift (S O) d x0) d H8 (Flat Cast) t3 (lift (S O) d x2) H12) (lift (S O) d -(THead (Flat Cast) x0 x2)) (lift_flat Cast x0 x2 (S O) d)) H8 (ty3_cast g a -x2 x0 H15 x1 H10)))))))) H11))))))) H7)))))))))))))))))) c t1 t2 H))))). +y1)))) (\lambda (_: T).(\lambda (y2: T).(subst1 d u (THead (Flat Cast) t0 t4) +(lift (S O) d y2)))) (\lambda (y1: T).(\lambda (y2: T).(ty3 g a y1 y2))) +(THead (Flat Cast) x0 x2) (THead (Flat Cast) x1 x0) (eq_ind_r T (THead (Flat +Cast) (lift (S O) d x0) (lift (S O) d x2)) (\lambda (t: T).(subst1 d u (THead +(Flat Cast) t4 t3) t)) (subst1_head u t4 (lift (S O) d x0) d H8 (Flat Cast) +t3 (lift (S O) d x2) H12) (lift (S O) d (THead (Flat Cast) x0 x2)) (lift_flat +Cast x0 x2 (S O) d)) (eq_ind_r T (THead (Flat Cast) (lift (S O) d x1) (lift +(S O) d x0)) (\lambda (t: T).(subst1 d u (THead (Flat Cast) t0 t4) t)) +(subst1_head u t0 (lift (S O) d x1) d H9 (Flat Cast) t4 (lift (S O) d x0) H8) +(lift (S O) d (THead (Flat Cast) x1 x0)) (lift_flat Cast x1 x0 (S O) d)) +(ty3_cast g a x2 x0 H15 x1 H10)))))))) H11))))))) H7)))))))))))))))))) c t1 +t2 H))))). theorem ty3_gen_cvoid: \forall (g: G).(\forall (c: C).(\forall (t1: T).(\forall (t2: T).((ty3 g c @@ -1103,47 +1109,59 @@ C).(\lambda (H5: (drop (S O) d c0 a)).(let H6 \def (H3 e u d H4 a H5) in (\lambda (_: T).(\lambda (y2: T).(eq T t0 (lift (S O) d y2)))) (\lambda (y1: T).(\lambda (y2: T).(ty3 g a y1 y2))) (ex3_2 T T (\lambda (y1: T).(\lambda (_: T).(eq T (THead (Flat Cast) t4 t3) (lift (S O) d y1)))) (\lambda (_: -T).(\lambda (y2: T).(eq T t4 (lift (S O) d y2)))) (\lambda (y1: T).(\lambda -(y2: T).(ty3 g a y1 y2)))) (\lambda (x0: T).(\lambda (x1: T).(\lambda (H7: -(eq T t4 (lift (S O) d x0))).(\lambda (H8: (eq T t0 (lift (S O) d -x1))).(\lambda (H9: (ty3 g a x0 x1)).(let H10 \def (eq_ind T t0 (\lambda (t: -T).(ty3 g c0 t4 t)) H2 (lift (S O) d x1) H8) in (let H11 \def (eq_ind T t4 -(\lambda (t: T).(ty3 g c0 t (lift (S O) d x1))) H10 (lift (S O) d x0) H7) in -(let H12 \def (eq_ind T t4 (\lambda (t: T).(\forall (e0: C).(\forall (u0: -T).(\forall (d0: nat).((getl d0 c0 (CHead e0 (Bind Void) u0)) \to (\forall -(a0: C).((drop (S O) d0 c0 a0) \to (ex3_2 T T (\lambda (y1: T).(\lambda (_: -T).(eq T t3 (lift (S O) d0 y1)))) (\lambda (_: T).(\lambda (y2: T).(eq T t -(lift (S O) d0 y2)))) (\lambda (y1: T).(\lambda (y2: T).(ty3 g a0 y1 -y2))))))))))) H1 (lift (S O) d x0) H7) in (let H13 \def (eq_ind T t4 (\lambda -(t: T).(ty3 g c0 t3 t)) H0 (lift (S O) d x0) H7) in (eq_ind_r T (lift (S O) d -x0) (\lambda (t: T).(ex3_2 T T (\lambda (y1: T).(\lambda (_: T).(eq T (THead -(Flat Cast) t t3) (lift (S O) d y1)))) (\lambda (_: T).(\lambda (y2: T).(eq T -t (lift (S O) d y2)))) (\lambda (y1: T).(\lambda (y2: T).(ty3 g a y1 y2))))) -(let H14 \def (H12 e u d H4 a H5) in (ex3_2_ind T T (\lambda (y1: T).(\lambda -(_: T).(eq T t3 (lift (S O) d y1)))) (\lambda (_: T).(\lambda (y2: T).(eq T -(lift (S O) d x0) (lift (S O) d y2)))) (\lambda (y1: T).(\lambda (y2: T).(ty3 -g a y1 y2))) (ex3_2 T T (\lambda (y1: T).(\lambda (_: T).(eq T (THead (Flat -Cast) (lift (S O) d x0) t3) (lift (S O) d y1)))) (\lambda (_: T).(\lambda -(y2: T).(eq T (lift (S O) d x0) (lift (S O) d y2)))) (\lambda (y1: -T).(\lambda (y2: T).(ty3 g a y1 y2)))) (\lambda (x2: T).(\lambda (x3: -T).(\lambda (H15: (eq T t3 (lift (S O) d x2))).(\lambda (H16: (eq T (lift (S -O) d x0) (lift (S O) d x3))).(\lambda (H17: (ty3 g a x2 x3)).(let H18 \def -(eq_ind T t3 (\lambda (t: T).(ty3 g c0 t (lift (S O) d x0))) H13 (lift (S O) -d x2) H15) in (eq_ind_r T (lift (S O) d x2) (\lambda (t: T).(ex3_2 T T -(\lambda (y1: T).(\lambda (_: T).(eq T (THead (Flat Cast) (lift (S O) d x0) -t) (lift (S O) d y1)))) (\lambda (_: T).(\lambda (y2: T).(eq T (lift (S O) d -x0) (lift (S O) d y2)))) (\lambda (y1: T).(\lambda (y2: T).(ty3 g a y1 -y2))))) (let H19 \def (eq_ind_r T x3 (\lambda (t: T).(ty3 g a x2 t)) H17 x0 -(lift_inj x0 x3 (S O) d H16)) in (eq_ind T (lift (S O) d (THead (Flat Cast) -x0 x2)) (\lambda (t: T).(ex3_2 T T (\lambda (y1: T).(\lambda (_: T).(eq T t -(lift (S O) d y1)))) (\lambda (_: T).(\lambda (y2: T).(eq T (lift (S O) d x0) -(lift (S O) d y2)))) (\lambda (y1: T).(\lambda (y2: T).(ty3 g a y1 y2))))) -(ex3_2_intro T T (\lambda (y1: T).(\lambda (_: T).(eq T (lift (S O) d (THead -(Flat Cast) x0 x2)) (lift (S O) d y1)))) (\lambda (_: T).(\lambda (y2: T).(eq -T (lift (S O) d x0) (lift (S O) d y2)))) (\lambda (y1: T).(\lambda (y2: -T).(ty3 g a y1 y2))) (THead (Flat Cast) x0 x2) x0 (refl_equal T (lift (S O) d -(THead (Flat Cast) x0 x2))) (refl_equal T (lift (S O) d x0)) (ty3_cast g a x2 -x0 H19 x1 H9)) (THead (Flat Cast) (lift (S O) d x0) (lift (S O) d x2)) -(lift_flat Cast x0 x2 (S O) d))) t3 H15))))))) H14)) t4 H7)))))))))) -H6)))))))))))))))) c t1 t2 H))))). +T).(\lambda (y2: T).(eq T (THead (Flat Cast) t0 t4) (lift (S O) d y2)))) +(\lambda (y1: T).(\lambda (y2: T).(ty3 g a y1 y2)))) (\lambda (x0: +T).(\lambda (x1: T).(\lambda (H7: (eq T t4 (lift (S O) d x0))).(\lambda (H8: +(eq T t0 (lift (S O) d x1))).(\lambda (H9: (ty3 g a x0 x1)).(let H10 \def +(eq_ind T t0 (\lambda (t: T).(ty3 g c0 t4 t)) H2 (lift (S O) d x1) H8) in +(eq_ind_r T (lift (S O) d x1) (\lambda (t: T).(ex3_2 T T (\lambda (y1: +T).(\lambda (_: T).(eq T (THead (Flat Cast) t4 t3) (lift (S O) d y1)))) +(\lambda (_: T).(\lambda (y2: T).(eq T (THead (Flat Cast) t t4) (lift (S O) d +y2)))) (\lambda (y1: T).(\lambda (y2: T).(ty3 g a y1 y2))))) (let H11 \def +(eq_ind T t4 (\lambda (t: T).(ty3 g c0 t (lift (S O) d x1))) H10 (lift (S O) +d x0) H7) in (let H12 \def (eq_ind T t4 (\lambda (t: T).(\forall (e0: +C).(\forall (u0: T).(\forall (d0: nat).((getl d0 c0 (CHead e0 (Bind Void) +u0)) \to (\forall (a0: C).((drop (S O) d0 c0 a0) \to (ex3_2 T T (\lambda (y1: +T).(\lambda (_: T).(eq T t3 (lift (S O) d0 y1)))) (\lambda (_: T).(\lambda +(y2: T).(eq T t (lift (S O) d0 y2)))) (\lambda (y1: T).(\lambda (y2: T).(ty3 +g a0 y1 y2))))))))))) H1 (lift (S O) d x0) H7) in (let H13 \def (eq_ind T t4 +(\lambda (t: T).(ty3 g c0 t3 t)) H0 (lift (S O) d x0) H7) in (eq_ind_r T +(lift (S O) d x0) (\lambda (t: T).(ex3_2 T T (\lambda (y1: T).(\lambda (_: +T).(eq T (THead (Flat Cast) t t3) (lift (S O) d y1)))) (\lambda (_: +T).(\lambda (y2: T).(eq T (THead (Flat Cast) (lift (S O) d x1) t) (lift (S O) +d y2)))) (\lambda (y1: T).(\lambda (y2: T).(ty3 g a y1 y2))))) (let H14 \def +(H12 e u d H4 a H5) in (ex3_2_ind T T (\lambda (y1: T).(\lambda (_: T).(eq T +t3 (lift (S O) d y1)))) (\lambda (_: T).(\lambda (y2: T).(eq T (lift (S O) d +x0) (lift (S O) d y2)))) (\lambda (y1: T).(\lambda (y2: T).(ty3 g a y1 y2))) +(ex3_2 T T (\lambda (y1: T).(\lambda (_: T).(eq T (THead (Flat Cast) (lift (S +O) d x0) t3) (lift (S O) d y1)))) (\lambda (_: T).(\lambda (y2: T).(eq T +(THead (Flat Cast) (lift (S O) d x1) (lift (S O) d x0)) (lift (S O) d y2)))) +(\lambda (y1: T).(\lambda (y2: T).(ty3 g a y1 y2)))) (\lambda (x2: +T).(\lambda (x3: T).(\lambda (H15: (eq T t3 (lift (S O) d x2))).(\lambda +(H16: (eq T (lift (S O) d x0) (lift (S O) d x3))).(\lambda (H17: (ty3 g a x2 +x3)).(let H18 \def (eq_ind T t3 (\lambda (t: T).(ty3 g c0 t (lift (S O) d +x0))) H13 (lift (S O) d x2) H15) in (eq_ind_r T (lift (S O) d x2) (\lambda +(t: T).(ex3_2 T T (\lambda (y1: T).(\lambda (_: T).(eq T (THead (Flat Cast) +(lift (S O) d x0) t) (lift (S O) d y1)))) (\lambda (_: T).(\lambda (y2: +T).(eq T (THead (Flat Cast) (lift (S O) d x1) (lift (S O) d x0)) (lift (S O) +d y2)))) (\lambda (y1: T).(\lambda (y2: T).(ty3 g a y1 y2))))) (let H19 \def +(eq_ind_r T x3 (\lambda (t: T).(ty3 g a x2 t)) H17 x0 (lift_inj x0 x3 (S O) d +H16)) in (eq_ind T (lift (S O) d (THead (Flat Cast) x0 x2)) (\lambda (t: +T).(ex3_2 T T (\lambda (y1: T).(\lambda (_: T).(eq T t (lift (S O) d y1)))) +(\lambda (_: T).(\lambda (y2: T).(eq T (THead (Flat Cast) (lift (S O) d x1) +(lift (S O) d x0)) (lift (S O) d y2)))) (\lambda (y1: T).(\lambda (y2: +T).(ty3 g a y1 y2))))) (eq_ind T (lift (S O) d (THead (Flat Cast) x1 x0)) +(\lambda (t: T).(ex3_2 T T (\lambda (y1: T).(\lambda (_: T).(eq T (lift (S O) +d (THead (Flat Cast) x0 x2)) (lift (S O) d y1)))) (\lambda (_: T).(\lambda +(y2: T).(eq T t (lift (S O) d y2)))) (\lambda (y1: T).(\lambda (y2: T).(ty3 g +a y1 y2))))) (ex3_2_intro T T (\lambda (y1: T).(\lambda (_: T).(eq T (lift (S +O) d (THead (Flat Cast) x0 x2)) (lift (S O) d y1)))) (\lambda (_: T).(\lambda +(y2: T).(eq T (lift (S O) d (THead (Flat Cast) x1 x0)) (lift (S O) d y2)))) +(\lambda (y1: T).(\lambda (y2: T).(ty3 g a y1 y2))) (THead (Flat Cast) x0 x2) +(THead (Flat Cast) x1 x0) (refl_equal T (lift (S O) d (THead (Flat Cast) x0 +x2))) (refl_equal T (lift (S O) d (THead (Flat Cast) x1 x0))) (ty3_cast g a +x2 x0 H19 x1 H9)) (THead (Flat Cast) (lift (S O) d x1) (lift (S O) d x0)) +(lift_flat Cast x1 x0 (S O) d)) (THead (Flat Cast) (lift (S O) d x0) (lift (S +O) d x2)) (lift_flat Cast x0 x2 (S O) d))) t3 H15))))))) H14)) t4 H7)))) t0 +H8))))))) H6)))))))))))))))) c t1 t2 H))))). diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/tau0.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/tau0.ma index 8bc71a82e..a9fb878ea 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/tau0.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/tau0.ma @@ -622,13 +622,13 @@ v2)).(\lambda (H16: (tau0 g c0 t2 t6)).(let H_y \def (H1 t6 H16) in (let H_y0 t2) (THead (Flat Cast) v2 t6)) (\lambda (x: T).(\lambda (H18: (ty3 g c0 v2 x)).(ex_ind T (\lambda (t: T).(ty3 g c0 t6 t)) (ty3 g c0 (THead (Flat Cast) t3 t2) (THead (Flat Cast) v2 t6)) (\lambda (x0: T).(\lambda (H19: (ty3 g c0 -t6 x0)).(ty3_conv g c0 (THead (Flat Cast) v2 t6) v2 (ty3_cast g c0 t6 v2 -(ty3_sconv g c0 t6 x0 H19 t3 v2 H_y0 H17) x H18) (THead (Flat Cast) t3 t2) t3 -(ty3_cast g c0 t2 t3 H0 v2 H_y0) (pc3_s c0 t3 (THead (Flat Cast) v2 t6) -(pc3_pr2_u c0 t6 (THead (Flat Cast) v2 t6) (pr2_free c0 (THead (Flat Cast) v2 -t6) t6 (pr0_epsilon t6 t6 (pr0_refl t6) v2)) t3 H17))))) (ty3_correct g c0 t2 -t6 H_y)))) (ty3_correct g c0 t3 v2 H_y0))))))) t4 H14)) t5 (sym_eq T t5 t2 -H13))) v1 (sym_eq T v1 t3 H12))) H11))) c1 (sym_eq C c1 c0 H7) H8 H9 H5 -H6))))]) in (H5 (refl_equal C c0) (refl_equal T (THead (Flat Cast) t3 t2)) -(refl_equal T t4))))))))))))) c u t1 H))))). +t6 x0)).(ty3_conv g c0 (THead (Flat Cast) v2 t6) (THead (Flat Cast) x v2) +(ty3_cast g c0 t6 v2 (ty3_sconv g c0 t6 x0 H19 t3 v2 H_y0 H17) x H18) (THead +(Flat Cast) t3 t2) (THead (Flat Cast) v2 t3) (ty3_cast g c0 t2 t3 H0 v2 H_y0) +(pc3_s c0 (THead (Flat Cast) v2 t3) (THead (Flat Cast) v2 t6) (pc3_thin_dx c0 +t6 t3 H17 v2 Cast))))) (ty3_correct g c0 t2 t6 H_y)))) (ty3_correct g c0 t3 +v2 H_y0))))))) t4 H14)) t5 (sym_eq T t5 t2 H13))) v1 (sym_eq T v1 t3 H12))) +H11))) c1 (sym_eq C c1 c0 H7) H8 H9 H5 H6))))]) in (H5 (refl_equal C c0) +(refl_equal T (THead (Flat Cast) t3 t2)) (refl_equal T t4))))))))))))) c u t1 +H))))). -- 2.39.2