From: Ferruccio Guidi Date: Thu, 5 Mar 2015 15:24:14 +0000 (+0000) Subject: basic_1: COMMIT COMPLETED X-Git-Tag: make_still_working~731 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=7efd72a7efa0e709d6395b2020a7995f7d3a2f89;p=helm.git basic_1: COMMIT COMPLETED - component wf3 - additional files basic_2: some corrections --- diff --git a/matita/matita/contribs/lambdadelta/basic_1/definitions.ma b/matita/matita/contribs/lambdadelta/basic_1/definitions.ma index 5863b4243..010b9d252 100644 --- a/matita/matita/contribs/lambdadelta/basic_1/definitions.ma +++ b/matita/matita/contribs/lambdadelta/basic_1/definitions.ma @@ -14,55 +14,55 @@ (* This file was automatically generated: do not edit *********************) -include "Basic-1/tlt/defs.ma". +include "basic_1/tlt/defs.ma". -include "Basic-1/iso/defs.ma". +include "basic_1/iso/defs.ma". -include "Basic-1/clen/defs.ma". +include "basic_1/clen/defs.ma". -include "Basic-1/flt/defs.ma". +include "basic_1/flt/defs.ma". -include "Basic-1/app/defs.ma". +include "basic_1/app/defs.ma". -include "Basic-1/cnt/defs.ma". +include "basic_1/cnt/defs.ma". -include "Basic-1/cimp/defs.ma". +include "basic_1/cimp/defs.ma". -include "Basic-1/csubv/defs.ma". +include "basic_1/subst1/defs.ma". -include "Basic-1/subst/defs.ma". +include "basic_1/subst/defs.ma". -include "Basic-1/subst1/defs.ma". +include "basic_1/csubst1/defs.ma". -include "Basic-1/csubst1/defs.ma". +include "basic_1/fsubst0/defs.ma". -include "Basic-1/fsubst0/defs.ma". +include "basic_1/next_plus/defs.ma". -include "Basic-1/next_plus/defs.ma". +include "basic_1/sty1/defs.ma". -include "Basic-1/sty1/defs.ma". +include "basic_1/llt/defs.ma". -include "Basic-1/llt/defs.ma". +include "basic_1/aprem/defs.ma". -include "Basic-1/aprem/defs.ma". +include "basic_1/ex0/defs.ma". -include "Basic-1/ex0/defs.ma". +include "basic_1/wcpr0/defs.ma". -include "Basic-1/wcpr0/defs.ma". +include "basic_1/csubv/defs.ma". -include "Basic-1/csuba/defs.ma". +include "basic_1/csuba/defs.ma". -include "Basic-1/nf2/defs.ma". +include "basic_1/nf2/defs.ma". -include "Basic-1/ex2/defs.ma". +include "basic_1/ex2/defs.ma". -include "Basic-1/csubc/defs.ma". +include "basic_1/csubc/defs.ma". -include "Basic-1/pc1/defs.ma". +include "basic_1/pc1/defs.ma". -include "Basic-1/ex1/defs.ma". +include "basic_1/ex1/defs.ma". -include "Basic-1/csubt/defs.ma". +include "basic_1/csubt/defs.ma". -include "Basic-1/wf3/defs.ma". +include "basic_1/wf3/defs.ma". diff --git a/matita/matita/contribs/lambdadelta/basic_1/planes.txt b/matita/matita/contribs/lambdadelta/basic_1/planes.txt new file mode 100644 index 000000000..d4b66b373 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_1/planes.txt @@ -0,0 +1,13 @@ +T s tlist tlt iso +C r flt app +lift cnt drop clear getl clen cimp +lift1 drop1 +subst0 subst1 subst csubst0 csubst1 fsubst0 +G next_plus +sty0 sty1 +A asucc aplus leq llt aprem ex0 +pr0 wcpr0 pr1 pr2 pr3 +csubv arity csuba +nf2 sn3 sc3 csubc ex2 +pc1 pc3 +ty3 csubt wf3 ex1 diff --git a/matita/matita/contribs/lambdadelta/basic_1/spare.ma b/matita/matita/contribs/lambdadelta/basic_1/spare.ma index 95d2c24ee..58a624eef 100644 --- a/matita/matita/contribs/lambdadelta/basic_1/spare.ma +++ b/matita/matita/contribs/lambdadelta/basic_1/spare.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -include "Basic-1/theory.ma". +include "basic_1/theory.ma". axiom pc3_gen_appls_sort_abst: \forall (c: C).(\forall (vs: TList).(\forall (w: T).(\forall (u: T).(\forall diff --git a/matita/matita/contribs/lambdadelta/basic_1/theory.ma b/matita/matita/contribs/lambdadelta/basic_1/theory.ma index f405be588..771c60e75 100644 --- a/matita/matita/contribs/lambdadelta/basic_1/theory.ma +++ b/matita/matita/contribs/lambdadelta/basic_1/theory.ma @@ -14,29 +14,27 @@ (* This file was automatically generated: do not edit *********************) -include "Basic-1/subst0/tlt.ma". +include "basic_1/subst0/tlt.ma". -include "Basic-1/subst/props.ma". +include "basic_1/subst/props.ma". -include "Basic-1/sty1/cnt.ma". +include "basic_1/sty1/cnt.ma". -include "Basic-1/ex0/props.ma". +include "basic_1/ex0/props.ma". -include "Basic-1/wcpr0/fwd.ma". +include "basic_1/pr3/wcpr0.ma". -include "Basic-1/pr3/wcpr0.ma". +include "basic_1/ex2/props.ma". -include "Basic-1/ex2/props.ma". +include "basic_1/ex1/props.ma". -include "Basic-1/ex1/props.ma". +include "basic_1/ty3/sty0.ma". -include "Basic-1/ty3/sty0.ma". +include "basic_1/csubt/csuba.ma". -include "Basic-1/csubt/csuba.ma". +include "basic_1/ty3/fwd_nf2.ma". -include "Basic-1/ty3/fwd_nf2.ma". +include "basic_1/ty3/nf2.ma". -include "Basic-1/ty3/nf2.ma". - -include "Basic-1/wf3/props.ma". +include "basic_1/wf3/props.ma". diff --git a/matita/matita/contribs/lambdadelta/basic_1/wf3/clear.ma b/matita/matita/contribs/lambdadelta/basic_1/wf3/clear.ma index b2ddd47af..4eb5de99c 100644 --- a/matita/matita/contribs/lambdadelta/basic_1/wf3/clear.ma +++ b/matita/matita/contribs/lambdadelta/basic_1/wf3/clear.ma @@ -14,78 +14,113 @@ (* This file was automatically generated: do not edit *********************) -include "Basic-1/wf3/fwd.ma". +include "basic_1/wf3/fwd.ma". + +include "basic_1/clear/fwd.ma". theorem wf3_clear_conf: \forall (c1: C).(\forall (c: C).((clear c1 c) \to (\forall (g: G).(\forall (c2: C).((wf3 g c1 c2) \to (wf3 g c c2)))))) \def - \lambda (c1: C).(\lambda (c: C).(\lambda (H: (clear c1 c)).(clear_ind + \lambda (c1: C).(\lambda (c: C).(\lambda (H: (clear c1 c)).(let TMP_1 \def (\lambda (c0: C).(\lambda (c2: C).(\forall (g: G).(\forall (c3: C).((wf3 g c0 -c3) \to (wf3 g c2 c3)))))) (\lambda (b: B).(\lambda (e: C).(\lambda (u: -T).(\lambda (g: G).(\lambda (c2: C).(\lambda (H0: (wf3 g (CHead e (Bind b) u) -c2)).H0)))))) (\lambda (e: C).(\lambda (c0: C).(\lambda (_: (clear e -c0)).(\lambda (H1: ((\forall (g: G).(\forall (c2: C).((wf3 g e c2) \to (wf3 g -c0 c2)))))).(\lambda (f: F).(\lambda (u: T).(\lambda (g: G).(\lambda (c2: -C).(\lambda (H2: (wf3 g (CHead e (Flat f) u) c2)).(let H_y \def -(wf3_gen_flat1 g e c2 u f H2) in (H1 g c2 H_y))))))))))) c1 c H))). -(* COMMENTS -Initial nodes: 145 -END *) +c3) \to (wf3 g c2 c3)))))) in (let TMP_2 \def (\lambda (b: B).(\lambda (e: +C).(\lambda (u: T).(\lambda (g: G).(\lambda (c2: C).(\lambda (H0: (wf3 g +(CHead e (Bind b) u) c2)).H0)))))) in (let TMP_3 \def (\lambda (e: +C).(\lambda (c0: C).(\lambda (_: (clear e c0)).(\lambda (H1: ((\forall (g: +G).(\forall (c2: C).((wf3 g e c2) \to (wf3 g c0 c2)))))).(\lambda (f: +F).(\lambda (u: T).(\lambda (g: G).(\lambda (c2: C).(\lambda (H2: (wf3 g +(CHead e (Flat f) u) c2)).(let H_y \def (wf3_gen_flat1 g e c2 u f H2) in (H1 +g c2 H_y))))))))))) in (clear_ind TMP_1 TMP_2 TMP_3 c1 c H)))))). theorem clear_wf3_trans: \forall (c1: C).(\forall (d1: C).((clear c1 d1) \to (\forall (g: G).(\forall (d2: C).((wf3 g d1 d2) \to (ex2 C (\lambda (c2: C).(wf3 g c1 c2)) (\lambda (c2: C).(clear c2 d2)))))))) \def - \lambda (c1: C).(\lambda (d1: C).(\lambda (H: (clear c1 d1)).(clear_ind + \lambda (c1: C).(\lambda (d1: C).(\lambda (H: (clear c1 d1)).(let TMP_3 \def (\lambda (c: C).(\lambda (c0: C).(\forall (g: G).(\forall (d2: C).((wf3 g c0 -d2) \to (ex2 C (\lambda (c2: C).(wf3 g c c2)) (\lambda (c2: C).(clear c2 -d2)))))))) (\lambda (b: B).(\lambda (e: C).(\lambda (u: T).(\lambda (g: -G).(\lambda (d2: C).(\lambda (H0: (wf3 g (CHead e (Bind b) u) d2)).(let H_x -\def (wf3_gen_bind1 g e d2 u b H0) in (let H1 \def H_x in (or_ind (ex3_2 C T -(\lambda (c2: C).(\lambda (_: T).(eq C d2 (CHead c2 (Bind b) u)))) (\lambda -(c2: C).(\lambda (_: T).(wf3 g e c2))) (\lambda (_: C).(\lambda (w: T).(ty3 g -e u w)))) (ex3 C (\lambda (c2: C).(eq C d2 (CHead c2 (Bind Void) (TSort O)))) -(\lambda (c2: C).(wf3 g e c2)) (\lambda (_: C).(\forall (w: T).((ty3 g e u w) -\to False)))) (ex2 C (\lambda (c2: C).(wf3 g (CHead e (Bind b) u) c2)) -(\lambda (c2: C).(clear c2 d2))) (\lambda (H2: (ex3_2 C T (\lambda (c2: +d2) \to (let TMP_1 \def (\lambda (c2: C).(wf3 g c c2)) in (let TMP_2 \def +(\lambda (c2: C).(clear c2 d2)) in (ex2 C TMP_1 TMP_2)))))))) in (let TMP_87 +\def (\lambda (b: B).(\lambda (e: C).(\lambda (u: T).(\lambda (g: G).(\lambda +(d2: C).(\lambda (H0: (wf3 g (CHead e (Bind b) u) d2)).(let H_x \def +(wf3_gen_bind1 g e d2 u b H0) in (let H1 \def H_x in (let TMP_6 \def (\lambda +(c2: C).(\lambda (_: T).(let TMP_4 \def (Bind b) in (let TMP_5 \def (CHead c2 +TMP_4 u) in (eq C d2 TMP_5))))) in (let TMP_7 \def (\lambda (c2: C).(\lambda +(_: T).(wf3 g e c2))) in (let TMP_8 \def (\lambda (_: C).(\lambda (w: T).(ty3 +g e u w))) in (let TMP_9 \def (ex3_2 C T TMP_6 TMP_7 TMP_8) in (let TMP_13 +\def (\lambda (c2: C).(let TMP_10 \def (Bind Void) in (let TMP_11 \def (TSort +O) in (let TMP_12 \def (CHead c2 TMP_10 TMP_11) in (eq C d2 TMP_12))))) in +(let TMP_14 \def (\lambda (c2: C).(wf3 g e c2)) in (let TMP_15 \def (\lambda +(_: C).(\forall (w: T).((ty3 g e u w) \to False))) in (let TMP_16 \def (ex3 C +TMP_13 TMP_14 TMP_15) in (let TMP_19 \def (\lambda (c2: C).(let TMP_17 \def +(Bind b) in (let TMP_18 \def (CHead e TMP_17 u) in (wf3 g TMP_18 c2)))) in +(let TMP_20 \def (\lambda (c2: C).(clear c2 d2)) in (let TMP_21 \def (ex2 C +TMP_19 TMP_20) in (let TMP_51 \def (\lambda (H2: (ex3_2 C T (\lambda (c2: C).(\lambda (_: T).(eq C d2 (CHead c2 (Bind b) u)))) (\lambda (c2: C).(\lambda (_: T).(wf3 g e c2))) (\lambda (_: C).(\lambda (w: T).(ty3 g e u -w))))).(ex3_2_ind C T (\lambda (c2: C).(\lambda (_: T).(eq C d2 (CHead c2 -(Bind b) u)))) (\lambda (c2: C).(\lambda (_: T).(wf3 g e c2))) (\lambda (_: -C).(\lambda (w: T).(ty3 g e u w))) (ex2 C (\lambda (c2: C).(wf3 g (CHead e -(Bind b) u) c2)) (\lambda (c2: C).(clear c2 d2))) (\lambda (x0: C).(\lambda -(x1: T).(\lambda (H3: (eq C d2 (CHead x0 (Bind b) u))).(\lambda (H4: (wf3 g e -x0)).(\lambda (H5: (ty3 g e u x1)).(eq_ind_r C (CHead x0 (Bind b) u) (\lambda -(c: C).(ex2 C (\lambda (c2: C).(wf3 g (CHead e (Bind b) u) c2)) (\lambda (c2: -C).(clear c2 c)))) (ex_intro2 C (\lambda (c2: C).(wf3 g (CHead e (Bind b) u) -c2)) (\lambda (c2: C).(clear c2 (CHead x0 (Bind b) u))) (CHead x0 (Bind b) u) -(wf3_bind g e x0 H4 u x1 H5 b) (clear_bind b x0 u)) d2 H3)))))) H2)) (\lambda -(H2: (ex3 C (\lambda (c2: C).(eq C d2 (CHead c2 (Bind Void) (TSort O)))) -(\lambda (c2: C).(wf3 g e c2)) (\lambda (_: C).(\forall (w: T).((ty3 g e u w) -\to False))))).(ex3_ind C (\lambda (c2: C).(eq C d2 (CHead c2 (Bind Void) -(TSort O)))) (\lambda (c2: C).(wf3 g e c2)) (\lambda (_: C).(\forall (w: -T).((ty3 g e u w) \to False))) (ex2 C (\lambda (c2: C).(wf3 g (CHead e (Bind -b) u) c2)) (\lambda (c2: C).(clear c2 d2))) (\lambda (x0: C).(\lambda (H3: -(eq C d2 (CHead x0 (Bind Void) (TSort O)))).(\lambda (H4: (wf3 g e -x0)).(\lambda (H5: ((\forall (w: T).((ty3 g e u w) \to False)))).(eq_ind_r C -(CHead x0 (Bind Void) (TSort O)) (\lambda (c: C).(ex2 C (\lambda (c2: C).(wf3 -g (CHead e (Bind b) u) c2)) (\lambda (c2: C).(clear c2 c)))) (ex_intro2 C -(\lambda (c2: C).(wf3 g (CHead e (Bind b) u) c2)) (\lambda (c2: C).(clear c2 -(CHead x0 (Bind Void) (TSort O)))) (CHead x0 (Bind Void) (TSort O)) (wf3_void -g e x0 H4 u H5 b) (clear_bind Void x0 (TSort O))) d2 H3))))) H2)) H1))))))))) -(\lambda (e: C).(\lambda (c: C).(\lambda (_: (clear e c)).(\lambda (H1: -((\forall (g: G).(\forall (d2: C).((wf3 g c d2) \to (ex2 C (\lambda (c2: -C).(wf3 g e c2)) (\lambda (c2: C).(clear c2 d2)))))))).(\lambda (f: -F).(\lambda (u: T).(\lambda (g: G).(\lambda (d2: C).(\lambda (H2: (wf3 g c -d2)).(let H_x \def (H1 g d2 H2) in (let H3 \def H_x in (ex2_ind C (\lambda -(c2: C).(wf3 g e c2)) (\lambda (c2: C).(clear c2 d2)) (ex2 C (\lambda (c2: -C).(wf3 g (CHead e (Flat f) u) c2)) (\lambda (c2: C).(clear c2 d2))) (\lambda -(x: C).(\lambda (H4: (wf3 g e x)).(\lambda (H5: (clear x d2)).(ex_intro2 C -(\lambda (c2: C).(wf3 g (CHead e (Flat f) u) c2)) (\lambda (c2: C).(clear c2 -d2)) x (wf3_flat g e x H4 u f) H5)))) H3)))))))))))) c1 d1 H))). -(* COMMENTS -Initial nodes: 1023 -END *) +w))))).(let TMP_24 \def (\lambda (c2: C).(\lambda (_: T).(let TMP_22 \def +(Bind b) in (let TMP_23 \def (CHead c2 TMP_22 u) in (eq C d2 TMP_23))))) in +(let TMP_25 \def (\lambda (c2: C).(\lambda (_: T).(wf3 g e c2))) in (let +TMP_26 \def (\lambda (_: C).(\lambda (w: T).(ty3 g e u w))) in (let TMP_29 +\def (\lambda (c2: C).(let TMP_27 \def (Bind b) in (let TMP_28 \def (CHead e +TMP_27 u) in (wf3 g TMP_28 c2)))) in (let TMP_30 \def (\lambda (c2: C).(clear +c2 d2)) in (let TMP_31 \def (ex2 C TMP_29 TMP_30) in (let TMP_50 \def +(\lambda (x0: C).(\lambda (x1: T).(\lambda (H3: (eq C d2 (CHead x0 (Bind b) +u))).(\lambda (H4: (wf3 g e x0)).(\lambda (H5: (ty3 g e u x1)).(let TMP_32 +\def (Bind b) in (let TMP_33 \def (CHead x0 TMP_32 u) in (let TMP_38 \def +(\lambda (c: C).(let TMP_36 \def (\lambda (c2: C).(let TMP_34 \def (Bind b) +in (let TMP_35 \def (CHead e TMP_34 u) in (wf3 g TMP_35 c2)))) in (let TMP_37 +\def (\lambda (c2: C).(clear c2 c)) in (ex2 C TMP_36 TMP_37)))) in (let +TMP_41 \def (\lambda (c2: C).(let TMP_39 \def (Bind b) in (let TMP_40 \def +(CHead e TMP_39 u) in (wf3 g TMP_40 c2)))) in (let TMP_44 \def (\lambda (c2: +C).(let TMP_42 \def (Bind b) in (let TMP_43 \def (CHead x0 TMP_42 u) in +(clear c2 TMP_43)))) in (let TMP_45 \def (Bind b) in (let TMP_46 \def (CHead +x0 TMP_45 u) in (let TMP_47 \def (wf3_bind g e x0 H4 u x1 H5 b) in (let +TMP_48 \def (clear_bind b x0 u) in (let TMP_49 \def (ex_intro2 C TMP_41 +TMP_44 TMP_46 TMP_47 TMP_48) in (eq_ind_r C TMP_33 TMP_38 TMP_49 d2 +H3)))))))))))))))) in (ex3_2_ind C T TMP_24 TMP_25 TMP_26 TMP_31 TMP_50 +H2))))))))) in (let TMP_86 \def (\lambda (H2: (ex3 C (\lambda (c2: C).(eq C +d2 (CHead c2 (Bind Void) (TSort O)))) (\lambda (c2: C).(wf3 g e c2)) (\lambda +(_: C).(\forall (w: T).((ty3 g e u w) \to False))))).(let TMP_55 \def +(\lambda (c2: C).(let TMP_52 \def (Bind Void) in (let TMP_53 \def (TSort O) +in (let TMP_54 \def (CHead c2 TMP_52 TMP_53) in (eq C d2 TMP_54))))) in (let +TMP_56 \def (\lambda (c2: C).(wf3 g e c2)) in (let TMP_57 \def (\lambda (_: +C).(\forall (w: T).((ty3 g e u w) \to False))) in (let TMP_60 \def (\lambda +(c2: C).(let TMP_58 \def (Bind b) in (let TMP_59 \def (CHead e TMP_58 u) in +(wf3 g TMP_59 c2)))) in (let TMP_61 \def (\lambda (c2: C).(clear c2 d2)) in +(let TMP_62 \def (ex2 C TMP_60 TMP_61) in (let TMP_85 \def (\lambda (x0: +C).(\lambda (H3: (eq C d2 (CHead x0 (Bind Void) (TSort O)))).(\lambda (H4: +(wf3 g e x0)).(\lambda (H5: ((\forall (w: T).((ty3 g e u w) \to +False)))).(let TMP_63 \def (Bind Void) in (let TMP_64 \def (TSort O) in (let +TMP_65 \def (CHead x0 TMP_63 TMP_64) in (let TMP_70 \def (\lambda (c: C).(let +TMP_68 \def (\lambda (c2: C).(let TMP_66 \def (Bind b) in (let TMP_67 \def +(CHead e TMP_66 u) in (wf3 g TMP_67 c2)))) in (let TMP_69 \def (\lambda (c2: +C).(clear c2 c)) in (ex2 C TMP_68 TMP_69)))) in (let TMP_73 \def (\lambda +(c2: C).(let TMP_71 \def (Bind b) in (let TMP_72 \def (CHead e TMP_71 u) in +(wf3 g TMP_72 c2)))) in (let TMP_77 \def (\lambda (c2: C).(let TMP_74 \def +(Bind Void) in (let TMP_75 \def (TSort O) in (let TMP_76 \def (CHead x0 +TMP_74 TMP_75) in (clear c2 TMP_76))))) in (let TMP_78 \def (Bind Void) in +(let TMP_79 \def (TSort O) in (let TMP_80 \def (CHead x0 TMP_78 TMP_79) in +(let TMP_81 \def (wf3_void g e x0 H4 u H5 b) in (let TMP_82 \def (TSort O) in +(let TMP_83 \def (clear_bind Void x0 TMP_82) in (let TMP_84 \def (ex_intro2 C +TMP_73 TMP_77 TMP_80 TMP_81 TMP_83) in (eq_ind_r C TMP_65 TMP_70 TMP_84 d2 +H3)))))))))))))))))) in (ex3_ind C TMP_55 TMP_56 TMP_57 TMP_62 TMP_85 +H2))))))))) in (or_ind TMP_9 TMP_16 TMP_21 TMP_51 TMP_86 +H1)))))))))))))))))))))) in (let TMP_101 \def (\lambda (e: C).(\lambda (c: +C).(\lambda (_: (clear e c)).(\lambda (H1: ((\forall (g: G).(\forall (d2: +C).((wf3 g c d2) \to (ex2 C (\lambda (c2: C).(wf3 g e c2)) (\lambda (c2: +C).(clear c2 d2)))))))).(\lambda (f: F).(\lambda (u: T).(\lambda (g: +G).(\lambda (d2: C).(\lambda (H2: (wf3 g c d2)).(let H_x \def (H1 g d2 H2) in +(let H3 \def H_x in (let TMP_88 \def (\lambda (c2: C).(wf3 g e c2)) in (let +TMP_89 \def (\lambda (c2: C).(clear c2 d2)) in (let TMP_92 \def (\lambda (c2: +C).(let TMP_90 \def (Flat f) in (let TMP_91 \def (CHead e TMP_90 u) in (wf3 g +TMP_91 c2)))) in (let TMP_93 \def (\lambda (c2: C).(clear c2 d2)) in (let +TMP_94 \def (ex2 C TMP_92 TMP_93) in (let TMP_100 \def (\lambda (x: +C).(\lambda (H4: (wf3 g e x)).(\lambda (H5: (clear x d2)).(let TMP_97 \def +(\lambda (c2: C).(let TMP_95 \def (Flat f) in (let TMP_96 \def (CHead e +TMP_95 u) in (wf3 g TMP_96 c2)))) in (let TMP_98 \def (\lambda (c2: C).(clear +c2 d2)) in (let TMP_99 \def (wf3_flat g e x H4 u f) in (ex_intro2 C TMP_97 +TMP_98 x TMP_99 H5))))))) in (ex2_ind C TMP_88 TMP_89 TMP_94 TMP_100 +H3)))))))))))))))))) in (clear_ind TMP_3 TMP_87 TMP_101 c1 d1 H)))))). diff --git a/matita/matita/contribs/lambdadelta/basic_1/wf3/defs.ma b/matita/matita/contribs/lambdadelta/basic_1/wf3/defs.ma index a99661941..df5eedc6c 100644 --- a/matita/matita/contribs/lambdadelta/basic_1/wf3/defs.ma +++ b/matita/matita/contribs/lambdadelta/basic_1/wf3/defs.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -include "Basic-1/ty3/defs.ma". +include "basic_1/ty3/defs.ma". inductive wf3 (g: G): C \to (C \to Prop) \def | wf3_sort: \forall (m: nat).(wf3 g (CSort m) (CSort m)) diff --git a/matita/matita/contribs/lambdadelta/basic_1/wf3/fwd.ma b/matita/matita/contribs/lambdadelta/basic_1/wf3/fwd.ma index 71c903f06..62ecb8cc0 100644 --- a/matita/matita/contribs/lambdadelta/basic_1/wf3/fwd.ma +++ b/matita/matita/contribs/lambdadelta/basic_1/wf3/fwd.ma @@ -14,44 +14,71 @@ (* This file was automatically generated: do not edit *********************) -include "Basic-1/wf3/defs.ma". +include "basic_1/wf3/defs.ma". + +let rec wf3_ind (g: G) (P: (C \to (C \to Prop))) (f: (\forall (m: nat).(P +(CSort m) (CSort m)))) (f0: (\forall (c1: C).(\forall (c2: C).((wf3 g c1 c2) +\to ((P c1 c2) \to (\forall (u: T).(\forall (t: T).((ty3 g c1 u t) \to +(\forall (b: B).(P (CHead c1 (Bind b) u) (CHead c2 (Bind b) u))))))))))) (f1: +(\forall (c1: C).(\forall (c2: C).((wf3 g c1 c2) \to ((P c1 c2) \to (\forall +(u: T).(((\forall (t: T).((ty3 g c1 u t) \to False))) \to (\forall (b: B).(P +(CHead c1 (Bind b) u) (CHead c2 (Bind Void) (TSort O))))))))))) (f2: (\forall +(c1: C).(\forall (c2: C).((wf3 g c1 c2) \to ((P c1 c2) \to (\forall (u: +T).(\forall (f2: F).(P (CHead c1 (Flat f2) u) c2)))))))) (c: C) (c0: C) (w: +wf3 g c c0) on w: P c c0 \def match w with [(wf3_sort m) \Rightarrow (f m) | +(wf3_bind c1 c2 w0 u t t0 b) \Rightarrow (let TMP_3 \def ((wf3_ind g P f f0 +f1 f2) c1 c2 w0) in (f0 c1 c2 w0 TMP_3 u t t0 b)) | (wf3_void c1 c2 w0 u f3 +b) \Rightarrow (let TMP_2 \def ((wf3_ind g P f f0 f1 f2) c1 c2 w0) in (f1 c1 +c2 w0 TMP_2 u f3 b)) | (wf3_flat c1 c2 w0 u f3) \Rightarrow (let TMP_1 \def +((wf3_ind g P f f0 f1 f2) c1 c2 w0) in (f2 c1 c2 w0 TMP_1 u f3))]. theorem wf3_gen_sort1: \forall (g: G).(\forall (x: C).(\forall (m: nat).((wf3 g (CSort m) x) \to (eq C x (CSort m))))) \def \lambda (g: G).(\lambda (x: C).(\lambda (m: nat).(\lambda (H: (wf3 g (CSort -m) x)).(insert_eq C (CSort m) (\lambda (c: C).(wf3 g c x)) (\lambda (c: -C).(eq C x c)) (\lambda (y: C).(\lambda (H0: (wf3 g y x)).(wf3_ind g (\lambda -(c: C).(\lambda (c0: C).((eq C c (CSort m)) \to (eq C c0 c)))) (\lambda (m0: -nat).(\lambda (H1: (eq C (CSort m0) (CSort m))).(let H2 \def (f_equal C nat -(\lambda (e: C).(match e in C return (\lambda (_: C).nat) with [(CSort n) -\Rightarrow n | (CHead _ _ _) \Rightarrow m0])) (CSort m0) (CSort m) H1) in -(eq_ind_r nat m (\lambda (n: nat).(eq C (CSort n) (CSort n))) (refl_equal C -(CSort m)) m0 H2)))) (\lambda (c1: C).(\lambda (c2: C).(\lambda (_: (wf3 g c1 +m) x)).(let TMP_1 \def (CSort m) in (let TMP_2 \def (\lambda (c: C).(wf3 g c +x)) in (let TMP_3 \def (\lambda (c: C).(eq C x c)) in (let TMP_43 \def +(\lambda (y: C).(\lambda (H0: (wf3 g y x)).(let TMP_4 \def (\lambda (c: +C).(\lambda (c0: C).((eq C c (CSort m)) \to (eq C c0 c)))) in (let TMP_13 +\def (\lambda (m0: nat).(\lambda (H1: (eq C (CSort m0) (CSort m))).(let TMP_5 +\def (\lambda (e: C).(match e with [(CSort n) \Rightarrow n | (CHead _ _ _) +\Rightarrow m0])) in (let TMP_6 \def (CSort m0) in (let TMP_7 \def (CSort m) +in (let H2 \def (f_equal C nat TMP_5 TMP_6 TMP_7 H1) in (let TMP_10 \def +(\lambda (n: nat).(let TMP_8 \def (CSort n) in (let TMP_9 \def (CSort n) in +(eq C TMP_8 TMP_9)))) in (let TMP_11 \def (CSort m) in (let TMP_12 \def +(refl_equal C TMP_11) in (eq_ind_r nat m TMP_10 TMP_12 m0 H2)))))))))) in +(let TMP_23 \def (\lambda (c1: C).(\lambda (c2: C).(\lambda (_: (wf3 g c1 c2)).(\lambda (_: (((eq C c1 (CSort m)) \to (eq C c2 c1)))).(\lambda (u: T).(\lambda (t: T).(\lambda (_: (ty3 g c1 u t)).(\lambda (b: B).(\lambda (H4: -(eq C (CHead c1 (Bind b) u) (CSort m))).(let H5 \def (eq_ind C (CHead c1 -(Bind b) u) (\lambda (ee: C).(match ee in C return (\lambda (_: C).Prop) with -[(CSort _) \Rightarrow False | (CHead _ _ _) \Rightarrow True])) I (CSort m) -H4) in (False_ind (eq C (CHead c2 (Bind b) u) (CHead c1 (Bind b) u)) -H5))))))))))) (\lambda (c1: C).(\lambda (c2: C).(\lambda (_: (wf3 g c1 +(eq C (CHead c1 (Bind b) u) (CSort m))).(let TMP_14 \def (Bind b) in (let +TMP_15 \def (CHead c1 TMP_14 u) in (let TMP_16 \def (\lambda (ee: C).(match +ee with [(CSort _) \Rightarrow False | (CHead _ _ _) \Rightarrow True])) in +(let TMP_17 \def (CSort m) in (let H5 \def (eq_ind C TMP_15 TMP_16 I TMP_17 +H4) in (let TMP_18 \def (Bind b) in (let TMP_19 \def (CHead c2 TMP_18 u) in +(let TMP_20 \def (Bind b) in (let TMP_21 \def (CHead c1 TMP_20 u) in (let +TMP_22 \def (eq C TMP_19 TMP_21) in (False_ind TMP_22 H5)))))))))))))))))))) +in (let TMP_34 \def (\lambda (c1: C).(\lambda (c2: C).(\lambda (_: (wf3 g c1 c2)).(\lambda (_: (((eq C c1 (CSort m)) \to (eq C c2 c1)))).(\lambda (u: T).(\lambda (_: ((\forall (t: T).((ty3 g c1 u t) \to False)))).(\lambda (b: -B).(\lambda (H4: (eq C (CHead c1 (Bind b) u) (CSort m))).(let H5 \def (eq_ind -C (CHead c1 (Bind b) u) (\lambda (ee: C).(match ee in C return (\lambda (_: -C).Prop) with [(CSort _) \Rightarrow False | (CHead _ _ _) \Rightarrow -True])) I (CSort m) H4) in (False_ind (eq C (CHead c2 (Bind Void) (TSort O)) -(CHead c1 (Bind b) u)) H5)))))))))) (\lambda (c1: C).(\lambda (c2: -C).(\lambda (_: (wf3 g c1 c2)).(\lambda (_: (((eq C c1 (CSort m)) \to (eq C -c2 c1)))).(\lambda (u: T).(\lambda (f: F).(\lambda (H3: (eq C (CHead c1 (Flat -f) u) (CSort m))).(let H4 \def (eq_ind C (CHead c1 (Flat f) u) (\lambda (ee: -C).(match ee in C return (\lambda (_: C).Prop) with [(CSort _) \Rightarrow -False | (CHead _ _ _) \Rightarrow True])) I (CSort m) H3) in (False_ind (eq C -c2 (CHead c1 (Flat f) u)) H4))))))))) y x H0))) H)))). -(* COMMENTS -Initial nodes: 523 -END *) +B).(\lambda (H4: (eq C (CHead c1 (Bind b) u) (CSort m))).(let TMP_24 \def +(Bind b) in (let TMP_25 \def (CHead c1 TMP_24 u) in (let TMP_26 \def (\lambda +(ee: C).(match ee with [(CSort _) \Rightarrow False | (CHead _ _ _) +\Rightarrow True])) in (let TMP_27 \def (CSort m) in (let H5 \def (eq_ind C +TMP_25 TMP_26 I TMP_27 H4) in (let TMP_28 \def (Bind Void) in (let TMP_29 +\def (TSort O) in (let TMP_30 \def (CHead c2 TMP_28 TMP_29) in (let TMP_31 +\def (Bind b) in (let TMP_32 \def (CHead c1 TMP_31 u) in (let TMP_33 \def (eq +C TMP_30 TMP_32) in (False_ind TMP_33 H5)))))))))))))))))))) in (let TMP_42 +\def (\lambda (c1: C).(\lambda (c2: C).(\lambda (_: (wf3 g c1 c2)).(\lambda +(_: (((eq C c1 (CSort m)) \to (eq C c2 c1)))).(\lambda (u: T).(\lambda (f: +F).(\lambda (H3: (eq C (CHead c1 (Flat f) u) (CSort m))).(let TMP_35 \def +(Flat f) in (let TMP_36 \def (CHead c1 TMP_35 u) in (let TMP_37 \def (\lambda +(ee: C).(match ee with [(CSort _) \Rightarrow False | (CHead _ _ _) +\Rightarrow True])) in (let TMP_38 \def (CSort m) in (let H4 \def (eq_ind C +TMP_36 TMP_37 I TMP_38 H3) in (let TMP_39 \def (Flat f) in (let TMP_40 \def +(CHead c1 TMP_39 u) in (let TMP_41 \def (eq C c2 TMP_40) in (False_ind TMP_41 +H4)))))))))))))))) in (wf3_ind g TMP_4 TMP_13 TMP_23 TMP_34 TMP_42 y x +H0)))))))) in (insert_eq C TMP_1 TMP_2 TMP_3 TMP_43 H)))))))). theorem wf3_gen_bind1: \forall (g: G).(\forall (c1: C).(\forall (x: C).(\forall (v: T).(\forall (b: @@ -63,249 +90,509 @@ C).(wf3 g c1 c2)) (\lambda (_: C).(\forall (w: T).((ty3 g c1 v w) \to False)))))))))) \def \lambda (g: G).(\lambda (c1: C).(\lambda (x: C).(\lambda (v: T).(\lambda (b: -B).(\lambda (H: (wf3 g (CHead c1 (Bind b) v) x)).(insert_eq C (CHead c1 (Bind -b) v) (\lambda (c: C).(wf3 g c x)) (\lambda (_: C).(or (ex3_2 C T (\lambda -(c2: C).(\lambda (_: T).(eq C x (CHead c2 (Bind b) v)))) (\lambda (c2: -C).(\lambda (_: T).(wf3 g c1 c2))) (\lambda (_: C).(\lambda (w: T).(ty3 g c1 -v w)))) (ex3 C (\lambda (c2: C).(eq C x (CHead c2 (Bind Void) (TSort O)))) -(\lambda (c2: C).(wf3 g c1 c2)) (\lambda (_: C).(\forall (w: T).((ty3 g c1 v -w) \to False)))))) (\lambda (y: C).(\lambda (H0: (wf3 g y x)).(wf3_ind g -(\lambda (c: C).(\lambda (c0: C).((eq C c (CHead c1 (Bind b) v)) \to (or -(ex3_2 C T (\lambda (c2: C).(\lambda (_: T).(eq C c0 (CHead c2 (Bind b) v)))) -(\lambda (c2: C).(\lambda (_: T).(wf3 g c1 c2))) (\lambda (_: C).(\lambda (w: -T).(ty3 g c1 v w)))) (ex3 C (\lambda (c2: C).(eq C c0 (CHead c2 (Bind Void) -(TSort O)))) (\lambda (c2: C).(wf3 g c1 c2)) (\lambda (_: C).(\forall (w: -T).((ty3 g c1 v w) \to False)))))))) (\lambda (m: nat).(\lambda (H1: (eq C -(CSort m) (CHead c1 (Bind b) v))).(let H2 \def (eq_ind C (CSort m) (\lambda -(ee: C).(match ee in C return (\lambda (_: C).Prop) with [(CSort _) -\Rightarrow True | (CHead _ _ _) \Rightarrow False])) I (CHead c1 (Bind b) v) -H1) in (False_ind (or (ex3_2 C T (\lambda (c2: C).(\lambda (_: T).(eq C -(CSort m) (CHead c2 (Bind b) v)))) (\lambda (c2: C).(\lambda (_: T).(wf3 g c1 -c2))) (\lambda (_: C).(\lambda (w: T).(ty3 g c1 v w)))) (ex3 C (\lambda (c2: -C).(eq C (CSort m) (CHead c2 (Bind Void) (TSort O)))) (\lambda (c2: C).(wf3 g -c1 c2)) (\lambda (_: C).(\forall (w: T).((ty3 g c1 v w) \to False))))) H2)))) -(\lambda (c0: C).(\lambda (c2: C).(\lambda (H1: (wf3 g c0 c2)).(\lambda (H2: -(((eq C c0 (CHead c1 (Bind b) v)) \to (or (ex3_2 C T (\lambda (c3: -C).(\lambda (_: T).(eq C c2 (CHead c3 (Bind b) v)))) (\lambda (c3: -C).(\lambda (_: T).(wf3 g c1 c3))) (\lambda (_: C).(\lambda (w: T).(ty3 g c1 -v w)))) (ex3 C (\lambda (c3: C).(eq C c2 (CHead c3 (Bind Void) (TSort O)))) -(\lambda (c3: C).(wf3 g c1 c3)) (\lambda (_: C).(\forall (w: T).((ty3 g c1 v -w) \to False)))))))).(\lambda (u: T).(\lambda (t: T).(\lambda (H3: (ty3 g c0 -u t)).(\lambda (b0: B).(\lambda (H4: (eq C (CHead c0 (Bind b0) u) (CHead c1 -(Bind b) v))).(let H5 \def (f_equal C C (\lambda (e: C).(match e in C return -(\lambda (_: C).C) with [(CSort _) \Rightarrow c0 | (CHead c _ _) \Rightarrow -c])) (CHead c0 (Bind b0) u) (CHead c1 (Bind b) v) H4) in ((let H6 \def -(f_equal C B (\lambda (e: C).(match e in C return (\lambda (_: C).B) with -[(CSort _) \Rightarrow b0 | (CHead _ k _) \Rightarrow (match k in K return -(\lambda (_: K).B) with [(Bind b1) \Rightarrow b1 | (Flat _) \Rightarrow -b0])])) (CHead c0 (Bind b0) u) (CHead c1 (Bind b) v) H4) in ((let H7 \def -(f_equal C T (\lambda (e: C).(match e in C return (\lambda (_: C).T) with -[(CSort _) \Rightarrow u | (CHead _ _ t0) \Rightarrow t0])) (CHead c0 (Bind -b0) u) (CHead c1 (Bind b) v) H4) in (\lambda (H8: (eq B b0 b)).(\lambda (H9: -(eq C c0 c1)).(eq_ind_r B b (\lambda (b1: B).(or (ex3_2 C T (\lambda (c3: -C).(\lambda (_: T).(eq C (CHead c2 (Bind b1) u) (CHead c3 (Bind b) v)))) -(\lambda (c3: C).(\lambda (_: T).(wf3 g c1 c3))) (\lambda (_: C).(\lambda (w: -T).(ty3 g c1 v w)))) (ex3 C (\lambda (c3: C).(eq C (CHead c2 (Bind b1) u) -(CHead c3 (Bind Void) (TSort O)))) (\lambda (c3: C).(wf3 g c1 c3)) (\lambda -(_: C).(\forall (w: T).((ty3 g c1 v w) \to False)))))) (let H10 \def (eq_ind -T u (\lambda (t0: T).(ty3 g c0 t0 t)) H3 v H7) in (eq_ind_r T v (\lambda (t0: -T).(or (ex3_2 C T (\lambda (c3: C).(\lambda (_: T).(eq C (CHead c2 (Bind b) -t0) (CHead c3 (Bind b) v)))) (\lambda (c3: C).(\lambda (_: T).(wf3 g c1 c3))) -(\lambda (_: C).(\lambda (w: T).(ty3 g c1 v w)))) (ex3 C (\lambda (c3: C).(eq -C (CHead c2 (Bind b) t0) (CHead c3 (Bind Void) (TSort O)))) (\lambda (c3: -C).(wf3 g c1 c3)) (\lambda (_: C).(\forall (w: T).((ty3 g c1 v w) \to -False)))))) (let H11 \def (eq_ind C c0 (\lambda (c: C).(ty3 g c v t)) H10 c1 -H9) in (let H12 \def (eq_ind C c0 (\lambda (c: C).((eq C c (CHead c1 (Bind b) -v)) \to (or (ex3_2 C T (\lambda (c3: C).(\lambda (_: T).(eq C c2 (CHead c3 -(Bind b) v)))) (\lambda (c3: C).(\lambda (_: T).(wf3 g c1 c3))) (\lambda (_: -C).(\lambda (w: T).(ty3 g c1 v w)))) (ex3 C (\lambda (c3: C).(eq C c2 (CHead -c3 (Bind Void) (TSort O)))) (\lambda (c3: C).(wf3 g c1 c3)) (\lambda (_: -C).(\forall (w: T).((ty3 g c1 v w) \to False))))))) H2 c1 H9) in (let H13 -\def (eq_ind C c0 (\lambda (c: C).(wf3 g c c2)) H1 c1 H9) in (or_introl -(ex3_2 C T (\lambda (c3: C).(\lambda (_: T).(eq C (CHead c2 (Bind b) v) -(CHead c3 (Bind b) v)))) (\lambda (c3: C).(\lambda (_: T).(wf3 g c1 c3))) -(\lambda (_: C).(\lambda (w: T).(ty3 g c1 v w)))) (ex3 C (\lambda (c3: C).(eq -C (CHead c2 (Bind b) v) (CHead c3 (Bind Void) (TSort O)))) (\lambda (c3: -C).(wf3 g c1 c3)) (\lambda (_: C).(\forall (w: T).((ty3 g c1 v w) \to -False)))) (ex3_2_intro C T (\lambda (c3: C).(\lambda (_: T).(eq C (CHead c2 -(Bind b) v) (CHead c3 (Bind b) v)))) (\lambda (c3: C).(\lambda (_: T).(wf3 g -c1 c3))) (\lambda (_: C).(\lambda (w: T).(ty3 g c1 v w))) c2 t (refl_equal C -(CHead c2 (Bind b) v)) H13 H11))))) u H7)) b0 H8)))) H6)) H5))))))))))) -(\lambda (c0: C).(\lambda (c2: C).(\lambda (H1: (wf3 g c0 c2)).(\lambda (H2: -(((eq C c0 (CHead c1 (Bind b) v)) \to (or (ex3_2 C T (\lambda (c3: -C).(\lambda (_: T).(eq C c2 (CHead c3 (Bind b) v)))) (\lambda (c3: -C).(\lambda (_: T).(wf3 g c1 c3))) (\lambda (_: C).(\lambda (w: T).(ty3 g c1 -v w)))) (ex3 C (\lambda (c3: C).(eq C c2 (CHead c3 (Bind Void) (TSort O)))) -(\lambda (c3: C).(wf3 g c1 c3)) (\lambda (_: C).(\forall (w: T).((ty3 g c1 v -w) \to False)))))))).(\lambda (u: T).(\lambda (H3: ((\forall (t: T).((ty3 g -c0 u t) \to False)))).(\lambda (b0: B).(\lambda (H4: (eq C (CHead c0 (Bind -b0) u) (CHead c1 (Bind b) v))).(let H5 \def (f_equal C C (\lambda (e: -C).(match e in C return (\lambda (_: C).C) with [(CSort _) \Rightarrow c0 | -(CHead c _ _) \Rightarrow c])) (CHead c0 (Bind b0) u) (CHead c1 (Bind b) v) -H4) in ((let H6 \def (f_equal C B (\lambda (e: C).(match e in C return -(\lambda (_: C).B) with [(CSort _) \Rightarrow b0 | (CHead _ k _) \Rightarrow -(match k in K return (\lambda (_: K).B) with [(Bind b1) \Rightarrow b1 | -(Flat _) \Rightarrow b0])])) (CHead c0 (Bind b0) u) (CHead c1 (Bind b) v) H4) -in ((let H7 \def (f_equal C T (\lambda (e: C).(match e in C return (\lambda -(_: C).T) with [(CSort _) \Rightarrow u | (CHead _ _ t) \Rightarrow t])) -(CHead c0 (Bind b0) u) (CHead c1 (Bind b) v) H4) in (\lambda (_: (eq B b0 -b)).(\lambda (H9: (eq C c0 c1)).(let H10 \def (eq_ind T u (\lambda (t: -T).(\forall (t0: T).((ty3 g c0 t t0) \to False))) H3 v H7) in (let H11 \def -(eq_ind C c0 (\lambda (c: C).(\forall (t: T).((ty3 g c v t) \to False))) H10 -c1 H9) in (let H12 \def (eq_ind C c0 (\lambda (c: C).((eq C c (CHead c1 (Bind +B).(\lambda (H: (wf3 g (CHead c1 (Bind b) v) x)).(let TMP_1 \def (Bind b) in +(let TMP_2 \def (CHead c1 TMP_1 v) in (let TMP_3 \def (\lambda (c: C).(wf3 g +c x)) in (let TMP_17 \def (\lambda (_: C).(let TMP_6 \def (\lambda (c2: +C).(\lambda (_: T).(let TMP_4 \def (Bind b) in (let TMP_5 \def (CHead c2 +TMP_4 v) in (eq C x TMP_5))))) in (let TMP_7 \def (\lambda (c2: C).(\lambda +(_: T).(wf3 g c1 c2))) in (let TMP_8 \def (\lambda (_: C).(\lambda (w: +T).(ty3 g c1 v w))) in (let TMP_9 \def (ex3_2 C T TMP_6 TMP_7 TMP_8) in (let +TMP_13 \def (\lambda (c2: C).(let TMP_10 \def (Bind Void) in (let TMP_11 \def +(TSort O) in (let TMP_12 \def (CHead c2 TMP_10 TMP_11) in (eq C x TMP_12))))) +in (let TMP_14 \def (\lambda (c2: C).(wf3 g c1 c2)) in (let TMP_15 \def +(\lambda (_: C).(\forall (w: T).((ty3 g c1 v w) \to False))) in (let TMP_16 +\def (ex3 C TMP_13 TMP_14 TMP_15) in (or TMP_9 TMP_16)))))))))) in (let +TMP_242 \def (\lambda (y: C).(\lambda (H0: (wf3 g y x)).(let TMP_31 \def +(\lambda (c: C).(\lambda (c0: C).((eq C c (CHead c1 (Bind b) v)) \to (let +TMP_20 \def (\lambda (c2: C).(\lambda (_: T).(let TMP_18 \def (Bind b) in +(let TMP_19 \def (CHead c2 TMP_18 v) in (eq C c0 TMP_19))))) in (let TMP_21 +\def (\lambda (c2: C).(\lambda (_: T).(wf3 g c1 c2))) in (let TMP_22 \def +(\lambda (_: C).(\lambda (w: T).(ty3 g c1 v w))) in (let TMP_23 \def (ex3_2 C +T TMP_20 TMP_21 TMP_22) in (let TMP_27 \def (\lambda (c2: C).(let TMP_24 \def +(Bind Void) in (let TMP_25 \def (TSort O) in (let TMP_26 \def (CHead c2 +TMP_24 TMP_25) in (eq C c0 TMP_26))))) in (let TMP_28 \def (\lambda (c2: +C).(wf3 g c1 c2)) in (let TMP_29 \def (\lambda (_: C).(\forall (w: T).((ty3 g +c1 v w) \to False))) in (let TMP_30 \def (ex3 C TMP_27 TMP_28 TMP_29) in (or +TMP_23 TMP_30)))))))))))) in (let TMP_52 \def (\lambda (m: nat).(\lambda (H1: +(eq C (CSort m) (CHead c1 (Bind b) v))).(let TMP_32 \def (CSort m) in (let +TMP_33 \def (\lambda (ee: C).(match ee with [(CSort _) \Rightarrow True | +(CHead _ _ _) \Rightarrow False])) in (let TMP_34 \def (Bind b) in (let +TMP_35 \def (CHead c1 TMP_34 v) in (let H2 \def (eq_ind C TMP_32 TMP_33 I +TMP_35 H1) in (let TMP_39 \def (\lambda (c2: C).(\lambda (_: T).(let TMP_36 +\def (CSort m) in (let TMP_37 \def (Bind b) in (let TMP_38 \def (CHead c2 +TMP_37 v) in (eq C TMP_36 TMP_38)))))) in (let TMP_40 \def (\lambda (c2: +C).(\lambda (_: T).(wf3 g c1 c2))) in (let TMP_41 \def (\lambda (_: +C).(\lambda (w: T).(ty3 g c1 v w))) in (let TMP_42 \def (ex3_2 C T TMP_39 +TMP_40 TMP_41) in (let TMP_47 \def (\lambda (c2: C).(let TMP_43 \def (CSort +m) in (let TMP_44 \def (Bind Void) in (let TMP_45 \def (TSort O) in (let +TMP_46 \def (CHead c2 TMP_44 TMP_45) in (eq C TMP_43 TMP_46)))))) in (let +TMP_48 \def (\lambda (c2: C).(wf3 g c1 c2)) in (let TMP_49 \def (\lambda (_: +C).(\forall (w: T).((ty3 g c1 v w) \to False))) in (let TMP_50 \def (ex3 C +TMP_47 TMP_48 TMP_49) in (let TMP_51 \def (or TMP_42 TMP_50) in (False_ind +TMP_51 H2))))))))))))))))) in (let TMP_153 \def (\lambda (c0: C).(\lambda +(c2: C).(\lambda (H1: (wf3 g c0 c2)).(\lambda (H2: (((eq C c0 (CHead c1 (Bind b) v)) \to (or (ex3_2 C T (\lambda (c3: C).(\lambda (_: T).(eq C c2 (CHead c3 (Bind b) v)))) (\lambda (c3: C).(\lambda (_: T).(wf3 g c1 c3))) (\lambda (_: C).(\lambda (w: T).(ty3 g c1 v w)))) (ex3 C (\lambda (c3: C).(eq C c2 (CHead c3 (Bind Void) (TSort O)))) (\lambda (c3: C).(wf3 g c1 c3)) (\lambda (_: -C).(\forall (w: T).((ty3 g c1 v w) \to False))))))) H2 c1 H9) in (let H13 -\def (eq_ind C c0 (\lambda (c: C).(wf3 g c c2)) H1 c1 H9) in (or_intror -(ex3_2 C T (\lambda (c3: C).(\lambda (_: T).(eq C (CHead c2 (Bind Void) -(TSort O)) (CHead c3 (Bind b) v)))) (\lambda (c3: C).(\lambda (_: T).(wf3 g +C).(\forall (w: T).((ty3 g c1 v w) \to False)))))))).(\lambda (u: T).(\lambda +(t: T).(\lambda (H3: (ty3 g c0 u t)).(\lambda (b0: B).(\lambda (H4: (eq C +(CHead c0 (Bind b0) u) (CHead c1 (Bind b) v))).(let TMP_53 \def (\lambda (e: +C).(match e with [(CSort _) \Rightarrow c0 | (CHead c _ _) \Rightarrow c])) +in (let TMP_54 \def (Bind b0) in (let TMP_55 \def (CHead c0 TMP_54 u) in (let +TMP_56 \def (Bind b) in (let TMP_57 \def (CHead c1 TMP_56 v) in (let H5 \def +(f_equal C C TMP_53 TMP_55 TMP_57 H4) in (let TMP_58 \def (\lambda (e: +C).(match e with [(CSort _) \Rightarrow b0 | (CHead _ k _) \Rightarrow (match +k with [(Bind b1) \Rightarrow b1 | (Flat _) \Rightarrow b0])])) in (let +TMP_59 \def (Bind b0) in (let TMP_60 \def (CHead c0 TMP_59 u) in (let TMP_61 +\def (Bind b) in (let TMP_62 \def (CHead c1 TMP_61 v) in (let H6 \def +(f_equal C B TMP_58 TMP_60 TMP_62 H4) in (let TMP_63 \def (\lambda (e: +C).(match e with [(CSort _) \Rightarrow u | (CHead _ _ t0) \Rightarrow t0])) +in (let TMP_64 \def (Bind b0) in (let TMP_65 \def (CHead c0 TMP_64 u) in (let +TMP_66 \def (Bind b) in (let TMP_67 \def (CHead c1 TMP_66 v) in (let H7 \def +(f_equal C T TMP_63 TMP_65 TMP_67 H4) in (let TMP_151 \def (\lambda (H8: (eq +B b0 b)).(\lambda (H9: (eq C c0 c1)).(let TMP_85 \def (\lambda (b1: B).(let +TMP_72 \def (\lambda (c3: C).(\lambda (_: T).(let TMP_68 \def (Bind b1) in +(let TMP_69 \def (CHead c2 TMP_68 u) in (let TMP_70 \def (Bind b) in (let +TMP_71 \def (CHead c3 TMP_70 v) in (eq C TMP_69 TMP_71))))))) in (let TMP_73 +\def (\lambda (c3: C).(\lambda (_: T).(wf3 g c1 c3))) in (let TMP_74 \def +(\lambda (_: C).(\lambda (w: T).(ty3 g c1 v w))) in (let TMP_75 \def (ex3_2 C +T TMP_72 TMP_73 TMP_74) in (let TMP_81 \def (\lambda (c3: C).(let TMP_76 \def +(Bind b1) in (let TMP_77 \def (CHead c2 TMP_76 u) in (let TMP_78 \def (Bind +Void) in (let TMP_79 \def (TSort O) in (let TMP_80 \def (CHead c3 TMP_78 +TMP_79) in (eq C TMP_77 TMP_80))))))) in (let TMP_82 \def (\lambda (c3: +C).(wf3 g c1 c3)) in (let TMP_83 \def (\lambda (_: C).(\forall (w: T).((ty3 g +c1 v w) \to False))) in (let TMP_84 \def (ex3 C TMP_81 TMP_82 TMP_83) in (or +TMP_75 TMP_84)))))))))) in (let TMP_86 \def (\lambda (t0: T).(ty3 g c0 t0 t)) +in (let H10 \def (eq_ind T u TMP_86 H3 v H7) in (let TMP_104 \def (\lambda +(t0: T).(let TMP_91 \def (\lambda (c3: C).(\lambda (_: T).(let TMP_87 \def +(Bind b) in (let TMP_88 \def (CHead c2 TMP_87 t0) in (let TMP_89 \def (Bind +b) in (let TMP_90 \def (CHead c3 TMP_89 v) in (eq C TMP_88 TMP_90))))))) in +(let TMP_92 \def (\lambda (c3: C).(\lambda (_: T).(wf3 g c1 c3))) in (let +TMP_93 \def (\lambda (_: C).(\lambda (w: T).(ty3 g c1 v w))) in (let TMP_94 +\def (ex3_2 C T TMP_91 TMP_92 TMP_93) in (let TMP_100 \def (\lambda (c3: +C).(let TMP_95 \def (Bind b) in (let TMP_96 \def (CHead c2 TMP_95 t0) in (let +TMP_97 \def (Bind Void) in (let TMP_98 \def (TSort O) in (let TMP_99 \def +(CHead c3 TMP_97 TMP_98) in (eq C TMP_96 TMP_99))))))) in (let TMP_101 \def +(\lambda (c3: C).(wf3 g c1 c3)) in (let TMP_102 \def (\lambda (_: C).(\forall +(w: T).((ty3 g c1 v w) \to False))) in (let TMP_103 \def (ex3 C TMP_100 +TMP_101 TMP_102) in (or TMP_94 TMP_103)))))))))) in (let TMP_105 \def +(\lambda (c: C).(ty3 g c v t)) in (let H11 \def (eq_ind C c0 TMP_105 H10 c1 +H9) in (let TMP_119 \def (\lambda (c: C).((eq C c (CHead c1 (Bind b) v)) \to +(let TMP_108 \def (\lambda (c3: C).(\lambda (_: T).(let TMP_106 \def (Bind b) +in (let TMP_107 \def (CHead c3 TMP_106 v) in (eq C c2 TMP_107))))) in (let +TMP_109 \def (\lambda (c3: C).(\lambda (_: T).(wf3 g c1 c3))) in (let TMP_110 +\def (\lambda (_: C).(\lambda (w: T).(ty3 g c1 v w))) in (let TMP_111 \def +(ex3_2 C T TMP_108 TMP_109 TMP_110) in (let TMP_115 \def (\lambda (c3: +C).(let TMP_112 \def (Bind Void) in (let TMP_113 \def (TSort O) in (let +TMP_114 \def (CHead c3 TMP_112 TMP_113) in (eq C c2 TMP_114))))) in (let +TMP_116 \def (\lambda (c3: C).(wf3 g c1 c3)) in (let TMP_117 \def (\lambda +(_: C).(\forall (w: T).((ty3 g c1 v w) \to False))) in (let TMP_118 \def (ex3 +C TMP_115 TMP_116 TMP_117) in (or TMP_111 TMP_118))))))))))) in (let H12 \def +(eq_ind C c0 TMP_119 H2 c1 H9) in (let TMP_120 \def (\lambda (c: C).(wf3 g c +c2)) in (let H13 \def (eq_ind C c0 TMP_120 H1 c1 H9) in (let TMP_125 \def +(\lambda (c3: C).(\lambda (_: T).(let TMP_121 \def (Bind b) in (let TMP_122 +\def (CHead c2 TMP_121 v) in (let TMP_123 \def (Bind b) in (let TMP_124 \def +(CHead c3 TMP_123 v) in (eq C TMP_122 TMP_124))))))) in (let TMP_126 \def +(\lambda (c3: C).(\lambda (_: T).(wf3 g c1 c3))) in (let TMP_127 \def +(\lambda (_: C).(\lambda (w: T).(ty3 g c1 v w))) in (let TMP_128 \def (ex3_2 +C T TMP_125 TMP_126 TMP_127) in (let TMP_134 \def (\lambda (c3: C).(let +TMP_129 \def (Bind b) in (let TMP_130 \def (CHead c2 TMP_129 v) in (let +TMP_131 \def (Bind Void) in (let TMP_132 \def (TSort O) in (let TMP_133 \def +(CHead c3 TMP_131 TMP_132) in (eq C TMP_130 TMP_133))))))) in (let TMP_135 +\def (\lambda (c3: C).(wf3 g c1 c3)) in (let TMP_136 \def (\lambda (_: +C).(\forall (w: T).((ty3 g c1 v w) \to False))) in (let TMP_137 \def (ex3 C +TMP_134 TMP_135 TMP_136) in (let TMP_142 \def (\lambda (c3: C).(\lambda (_: +T).(let TMP_138 \def (Bind b) in (let TMP_139 \def (CHead c2 TMP_138 v) in +(let TMP_140 \def (Bind b) in (let TMP_141 \def (CHead c3 TMP_140 v) in (eq C +TMP_139 TMP_141))))))) in (let TMP_143 \def (\lambda (c3: C).(\lambda (_: +T).(wf3 g c1 c3))) in (let TMP_144 \def (\lambda (_: C).(\lambda (w: T).(ty3 +g c1 v w))) in (let TMP_145 \def (Bind b) in (let TMP_146 \def (CHead c2 +TMP_145 v) in (let TMP_147 \def (refl_equal C TMP_146) in (let TMP_148 \def +(ex3_2_intro C T TMP_142 TMP_143 TMP_144 c2 t TMP_147 H13 H11) in (let +TMP_149 \def (or_introl TMP_128 TMP_137 TMP_148) in (let TMP_150 \def +(eq_ind_r T v TMP_104 TMP_149 u H7) in (eq_ind_r B b TMP_85 TMP_150 b0 +H8)))))))))))))))))))))))))))))) in (let TMP_152 \def (TMP_151 H6) in +(TMP_152 H5)))))))))))))))))))))))))))))) in (let TMP_221 \def (\lambda (c0: +C).(\lambda (c2: C).(\lambda (H1: (wf3 g c0 c2)).(\lambda (H2: (((eq C c0 +(CHead c1 (Bind b) v)) \to (or (ex3_2 C T (\lambda (c3: C).(\lambda (_: +T).(eq C c2 (CHead c3 (Bind b) v)))) (\lambda (c3: C).(\lambda (_: T).(wf3 g c1 c3))) (\lambda (_: C).(\lambda (w: T).(ty3 g c1 v w)))) (ex3 C (\lambda -(c3: C).(eq C (CHead c2 (Bind Void) (TSort O)) (CHead c3 (Bind Void) (TSort -O)))) (\lambda (c3: C).(wf3 g c1 c3)) (\lambda (_: C).(\forall (w: T).((ty3 g -c1 v w) \to False)))) (ex3_intro C (\lambda (c3: C).(eq C (CHead c2 (Bind -Void) (TSort O)) (CHead c3 (Bind Void) (TSort O)))) (\lambda (c3: C).(wf3 g -c1 c3)) (\lambda (_: C).(\forall (w: T).((ty3 g c1 v w) \to False))) c2 -(refl_equal C (CHead c2 (Bind Void) (TSort O))) H13 H11))))))))) H6)) -H5)))))))))) (\lambda (c0: C).(\lambda (c2: C).(\lambda (_: (wf3 g c0 +(c3: C).(eq C c2 (CHead c3 (Bind Void) (TSort O)))) (\lambda (c3: C).(wf3 g +c1 c3)) (\lambda (_: C).(\forall (w: T).((ty3 g c1 v w) \to +False)))))))).(\lambda (u: T).(\lambda (H3: ((\forall (t: T).((ty3 g c0 u t) +\to False)))).(\lambda (b0: B).(\lambda (H4: (eq C (CHead c0 (Bind b0) u) +(CHead c1 (Bind b) v))).(let TMP_154 \def (\lambda (e: C).(match e with +[(CSort _) \Rightarrow c0 | (CHead c _ _) \Rightarrow c])) in (let TMP_155 +\def (Bind b0) in (let TMP_156 \def (CHead c0 TMP_155 u) in (let TMP_157 \def +(Bind b) in (let TMP_158 \def (CHead c1 TMP_157 v) in (let H5 \def (f_equal C +C TMP_154 TMP_156 TMP_158 H4) in (let TMP_159 \def (\lambda (e: C).(match e +with [(CSort _) \Rightarrow b0 | (CHead _ k _) \Rightarrow (match k with +[(Bind b1) \Rightarrow b1 | (Flat _) \Rightarrow b0])])) in (let TMP_160 \def +(Bind b0) in (let TMP_161 \def (CHead c0 TMP_160 u) in (let TMP_162 \def +(Bind b) in (let TMP_163 \def (CHead c1 TMP_162 v) in (let H6 \def (f_equal C +B TMP_159 TMP_161 TMP_163 H4) in (let TMP_164 \def (\lambda (e: C).(match e +with [(CSort _) \Rightarrow u | (CHead _ _ t) \Rightarrow t])) in (let +TMP_165 \def (Bind b0) in (let TMP_166 \def (CHead c0 TMP_165 u) in (let +TMP_167 \def (Bind b) in (let TMP_168 \def (CHead c1 TMP_167 v) in (let H7 +\def (f_equal C T TMP_164 TMP_166 TMP_168 H4) in (let TMP_219 \def (\lambda +(_: (eq B b0 b)).(\lambda (H9: (eq C c0 c1)).(let TMP_169 \def (\lambda (t: +T).(\forall (t0: T).((ty3 g c0 t t0) \to False))) in (let H10 \def (eq_ind T +u TMP_169 H3 v H7) in (let TMP_170 \def (\lambda (c: C).(\forall (t: T).((ty3 +g c v t) \to False))) in (let H11 \def (eq_ind C c0 TMP_170 H10 c1 H9) in +(let TMP_184 \def (\lambda (c: C).((eq C c (CHead c1 (Bind b) v)) \to (let +TMP_173 \def (\lambda (c3: C).(\lambda (_: T).(let TMP_171 \def (Bind b) in +(let TMP_172 \def (CHead c3 TMP_171 v) in (eq C c2 TMP_172))))) in (let +TMP_174 \def (\lambda (c3: C).(\lambda (_: T).(wf3 g c1 c3))) in (let TMP_175 +\def (\lambda (_: C).(\lambda (w: T).(ty3 g c1 v w))) in (let TMP_176 \def +(ex3_2 C T TMP_173 TMP_174 TMP_175) in (let TMP_180 \def (\lambda (c3: +C).(let TMP_177 \def (Bind Void) in (let TMP_178 \def (TSort O) in (let +TMP_179 \def (CHead c3 TMP_177 TMP_178) in (eq C c2 TMP_179))))) in (let +TMP_181 \def (\lambda (c3: C).(wf3 g c1 c3)) in (let TMP_182 \def (\lambda +(_: C).(\forall (w: T).((ty3 g c1 v w) \to False))) in (let TMP_183 \def (ex3 +C TMP_180 TMP_181 TMP_182) in (or TMP_176 TMP_183))))))))))) in (let H12 \def +(eq_ind C c0 TMP_184 H2 c1 H9) in (let TMP_185 \def (\lambda (c: C).(wf3 g c +c2)) in (let H13 \def (eq_ind C c0 TMP_185 H1 c1 H9) in (let TMP_191 \def +(\lambda (c3: C).(\lambda (_: T).(let TMP_186 \def (Bind Void) in (let +TMP_187 \def (TSort O) in (let TMP_188 \def (CHead c2 TMP_186 TMP_187) in +(let TMP_189 \def (Bind b) in (let TMP_190 \def (CHead c3 TMP_189 v) in (eq C +TMP_188 TMP_190)))))))) in (let TMP_192 \def (\lambda (c3: C).(\lambda (_: +T).(wf3 g c1 c3))) in (let TMP_193 \def (\lambda (_: C).(\lambda (w: T).(ty3 +g c1 v w))) in (let TMP_194 \def (ex3_2 C T TMP_191 TMP_192 TMP_193) in (let +TMP_201 \def (\lambda (c3: C).(let TMP_195 \def (Bind Void) in (let TMP_196 +\def (TSort O) in (let TMP_197 \def (CHead c2 TMP_195 TMP_196) in (let +TMP_198 \def (Bind Void) in (let TMP_199 \def (TSort O) in (let TMP_200 \def +(CHead c3 TMP_198 TMP_199) in (eq C TMP_197 TMP_200)))))))) in (let TMP_202 +\def (\lambda (c3: C).(wf3 g c1 c3)) in (let TMP_203 \def (\lambda (_: +C).(\forall (w: T).((ty3 g c1 v w) \to False))) in (let TMP_204 \def (ex3 C +TMP_201 TMP_202 TMP_203) in (let TMP_211 \def (\lambda (c3: C).(let TMP_205 +\def (Bind Void) in (let TMP_206 \def (TSort O) in (let TMP_207 \def (CHead +c2 TMP_205 TMP_206) in (let TMP_208 \def (Bind Void) in (let TMP_209 \def +(TSort O) in (let TMP_210 \def (CHead c3 TMP_208 TMP_209) in (eq C TMP_207 +TMP_210)))))))) in (let TMP_212 \def (\lambda (c3: C).(wf3 g c1 c3)) in (let +TMP_213 \def (\lambda (_: C).(\forall (w: T).((ty3 g c1 v w) \to False))) in +(let TMP_214 \def (Bind Void) in (let TMP_215 \def (TSort O) in (let TMP_216 +\def (CHead c2 TMP_214 TMP_215) in (let TMP_217 \def (refl_equal C TMP_216) +in (let TMP_218 \def (ex3_intro C TMP_211 TMP_212 TMP_213 c2 TMP_217 H13 H11) +in (or_intror TMP_194 TMP_204 TMP_218))))))))))))))))))))))))))) in (let +TMP_220 \def (TMP_219 H6) in (TMP_220 H5))))))))))))))))))))))))))))) in (let +TMP_241 \def (\lambda (c0: C).(\lambda (c2: C).(\lambda (_: (wf3 g c0 c2)).(\lambda (_: (((eq C c0 (CHead c1 (Bind b) v)) \to (or (ex3_2 C T (\lambda (c3: C).(\lambda (_: T).(eq C c2 (CHead c3 (Bind b) v)))) (\lambda (c3: C).(\lambda (_: T).(wf3 g c1 c3))) (\lambda (_: C).(\lambda (w: T).(ty3 g c1 v w)))) (ex3 C (\lambda (c3: C).(eq C c2 (CHead c3 (Bind Void) (TSort O)))) (\lambda (c3: C).(wf3 g c1 c3)) (\lambda (_: C).(\forall (w: T).((ty3 g c1 v w) \to False)))))))).(\lambda (u: T).(\lambda (f: F).(\lambda (H3: (eq C -(CHead c0 (Flat f) u) (CHead c1 (Bind b) v))).(let H4 \def (eq_ind C (CHead -c0 (Flat f) u) (\lambda (ee: C).(match ee in C return (\lambda (_: C).Prop) -with [(CSort _) \Rightarrow False | (CHead _ k _) \Rightarrow (match k in K -return (\lambda (_: K).Prop) with [(Bind _) \Rightarrow False | (Flat _) -\Rightarrow True])])) I (CHead c1 (Bind b) v) H3) in (False_ind (or (ex3_2 C -T (\lambda (c3: C).(\lambda (_: T).(eq C c2 (CHead c3 (Bind b) v)))) (\lambda -(c3: C).(\lambda (_: T).(wf3 g c1 c3))) (\lambda (_: C).(\lambda (w: T).(ty3 -g c1 v w)))) (ex3 C (\lambda (c3: C).(eq C c2 (CHead c3 (Bind Void) (TSort -O)))) (\lambda (c3: C).(wf3 g c1 c3)) (\lambda (_: C).(\forall (w: T).((ty3 g -c1 v w) \to False))))) H4))))))))) y x H0))) H)))))). -(* COMMENTS -Initial nodes: 2507 -END *) +(CHead c0 (Flat f) u) (CHead c1 (Bind b) v))).(let TMP_222 \def (Flat f) in +(let TMP_223 \def (CHead c0 TMP_222 u) in (let TMP_224 \def (\lambda (ee: +C).(match ee with [(CSort _) \Rightarrow False | (CHead _ k _) \Rightarrow +(match k with [(Bind _) \Rightarrow False | (Flat _) \Rightarrow True])])) in +(let TMP_225 \def (Bind b) in (let TMP_226 \def (CHead c1 TMP_225 v) in (let +H4 \def (eq_ind C TMP_223 TMP_224 I TMP_226 H3) in (let TMP_229 \def (\lambda +(c3: C).(\lambda (_: T).(let TMP_227 \def (Bind b) in (let TMP_228 \def +(CHead c3 TMP_227 v) in (eq C c2 TMP_228))))) in (let TMP_230 \def (\lambda +(c3: C).(\lambda (_: T).(wf3 g c1 c3))) in (let TMP_231 \def (\lambda (_: +C).(\lambda (w: T).(ty3 g c1 v w))) in (let TMP_232 \def (ex3_2 C T TMP_229 +TMP_230 TMP_231) in (let TMP_236 \def (\lambda (c3: C).(let TMP_233 \def +(Bind Void) in (let TMP_234 \def (TSort O) in (let TMP_235 \def (CHead c3 +TMP_233 TMP_234) in (eq C c2 TMP_235))))) in (let TMP_237 \def (\lambda (c3: +C).(wf3 g c1 c3)) in (let TMP_238 \def (\lambda (_: C).(\forall (w: T).((ty3 +g c1 v w) \to False))) in (let TMP_239 \def (ex3 C TMP_236 TMP_237 TMP_238) +in (let TMP_240 \def (or TMP_232 TMP_239) in (False_ind TMP_240 +H4))))))))))))))))))))))) in (wf3_ind g TMP_31 TMP_52 TMP_153 TMP_221 TMP_241 +y x H0)))))))) in (insert_eq C TMP_2 TMP_3 TMP_17 TMP_242 H))))))))))). theorem wf3_gen_flat1: \forall (g: G).(\forall (c1: C).(\forall (x: C).(\forall (v: T).(\forall (f: F).((wf3 g (CHead c1 (Flat f) v) x) \to (wf3 g c1 x)))))) \def \lambda (g: G).(\lambda (c1: C).(\lambda (x: C).(\lambda (v: T).(\lambda (f: -F).(\lambda (H: (wf3 g (CHead c1 (Flat f) v) x)).(insert_eq C (CHead c1 (Flat -f) v) (\lambda (c: C).(wf3 g c x)) (\lambda (_: C).(wf3 g c1 x)) (\lambda (y: -C).(\lambda (H0: (wf3 g y x)).(wf3_ind g (\lambda (c: C).(\lambda (c0: -C).((eq C c (CHead c1 (Flat f) v)) \to (wf3 g c1 c0)))) (\lambda (m: -nat).(\lambda (H1: (eq C (CSort m) (CHead c1 (Flat f) v))).(let H2 \def -(eq_ind C (CSort m) (\lambda (ee: C).(match ee in C return (\lambda (_: -C).Prop) with [(CSort _) \Rightarrow True | (CHead _ _ _) \Rightarrow -False])) I (CHead c1 (Flat f) v) H1) in (False_ind (wf3 g c1 (CSort m)) -H2)))) (\lambda (c0: C).(\lambda (c2: C).(\lambda (_: (wf3 g c0 c2)).(\lambda -(_: (((eq C c0 (CHead c1 (Flat f) v)) \to (wf3 g c1 c2)))).(\lambda (u: -T).(\lambda (t: T).(\lambda (_: (ty3 g c0 u t)).(\lambda (b: B).(\lambda (H4: -(eq C (CHead c0 (Bind b) u) (CHead c1 (Flat f) v))).(let H5 \def (eq_ind C -(CHead c0 (Bind b) u) (\lambda (ee: C).(match ee in C return (\lambda (_: -C).Prop) with [(CSort _) \Rightarrow False | (CHead _ k _) \Rightarrow (match -k in K return (\lambda (_: K).Prop) with [(Bind _) \Rightarrow True | (Flat -_) \Rightarrow False])])) I (CHead c1 (Flat f) v) H4) in (False_ind (wf3 g c1 -(CHead c2 (Bind b) u)) H5))))))))))) (\lambda (c0: C).(\lambda (c2: -C).(\lambda (_: (wf3 g c0 c2)).(\lambda (_: (((eq C c0 (CHead c1 (Flat f) v)) -\to (wf3 g c1 c2)))).(\lambda (u: T).(\lambda (_: ((\forall (t: T).((ty3 g c0 -u t) \to False)))).(\lambda (b: B).(\lambda (H4: (eq C (CHead c0 (Bind b) u) -(CHead c1 (Flat f) v))).(let H5 \def (eq_ind C (CHead c0 (Bind b) u) (\lambda -(ee: C).(match ee in C return (\lambda (_: C).Prop) with [(CSort _) -\Rightarrow False | (CHead _ k _) \Rightarrow (match k in K return (\lambda -(_: K).Prop) with [(Bind _) \Rightarrow True | (Flat _) \Rightarrow -False])])) I (CHead c1 (Flat f) v) H4) in (False_ind (wf3 g c1 (CHead c2 -(Bind Void) (TSort O))) H5)))))))))) (\lambda (c0: C).(\lambda (c2: -C).(\lambda (H1: (wf3 g c0 c2)).(\lambda (H2: (((eq C c0 (CHead c1 (Flat f) -v)) \to (wf3 g c1 c2)))).(\lambda (u: T).(\lambda (f0: F).(\lambda (H3: (eq C -(CHead c0 (Flat f0) u) (CHead c1 (Flat f) v))).(let H4 \def (f_equal C C -(\lambda (e: C).(match e in C return (\lambda (_: C).C) with [(CSort _) -\Rightarrow c0 | (CHead c _ _) \Rightarrow c])) (CHead c0 (Flat f0) u) (CHead -c1 (Flat f) v) H3) in ((let H5 \def (f_equal C F (\lambda (e: C).(match e in -C return (\lambda (_: C).F) with [(CSort _) \Rightarrow f0 | (CHead _ k _) -\Rightarrow (match k in K return (\lambda (_: K).F) with [(Bind _) -\Rightarrow f0 | (Flat f1) \Rightarrow f1])])) (CHead c0 (Flat f0) u) (CHead -c1 (Flat f) v) H3) in ((let H6 \def (f_equal C T (\lambda (e: C).(match e in -C return (\lambda (_: C).T) with [(CSort _) \Rightarrow u | (CHead _ _ t) -\Rightarrow t])) (CHead c0 (Flat f0) u) (CHead c1 (Flat f) v) H3) in (\lambda -(_: (eq F f0 f)).(\lambda (H8: (eq C c0 c1)).(let H9 \def (eq_ind C c0 -(\lambda (c: C).((eq C c (CHead c1 (Flat f) v)) \to (wf3 g c1 c2))) H2 c1 H8) -in (let H10 \def (eq_ind C c0 (\lambda (c: C).(wf3 g c c2)) H1 c1 H8) in -H10))))) H5)) H4))))))))) y x H0))) H)))))). -(* COMMENTS -Initial nodes: 737 -END *) +F).(\lambda (H: (wf3 g (CHead c1 (Flat f) v) x)).(let TMP_1 \def (Flat f) in +(let TMP_2 \def (CHead c1 TMP_1 v) in (let TMP_3 \def (\lambda (c: C).(wf3 g +c x)) in (let TMP_4 \def (\lambda (_: C).(wf3 g c1 x)) in (let TMP_52 \def +(\lambda (y: C).(\lambda (H0: (wf3 g y x)).(let TMP_5 \def (\lambda (c: +C).(\lambda (c0: C).((eq C c (CHead c1 (Flat f) v)) \to (wf3 g c1 c0)))) in +(let TMP_12 \def (\lambda (m: nat).(\lambda (H1: (eq C (CSort m) (CHead c1 +(Flat f) v))).(let TMP_6 \def (CSort m) in (let TMP_7 \def (\lambda (ee: +C).(match ee with [(CSort _) \Rightarrow True | (CHead _ _ _) \Rightarrow +False])) in (let TMP_8 \def (Flat f) in (let TMP_9 \def (CHead c1 TMP_8 v) in +(let H2 \def (eq_ind C TMP_6 TMP_7 I TMP_9 H1) in (let TMP_10 \def (CSort m) +in (let TMP_11 \def (wf3 g c1 TMP_10) in (False_ind TMP_11 H2)))))))))) in +(let TMP_21 \def (\lambda (c0: C).(\lambda (c2: C).(\lambda (_: (wf3 g c0 +c2)).(\lambda (_: (((eq C c0 (CHead c1 (Flat f) v)) \to (wf3 g c1 +c2)))).(\lambda (u: T).(\lambda (t: T).(\lambda (_: (ty3 g c0 u t)).(\lambda +(b: B).(\lambda (H4: (eq C (CHead c0 (Bind b) u) (CHead c1 (Flat f) v))).(let +TMP_13 \def (Bind b) in (let TMP_14 \def (CHead c0 TMP_13 u) in (let TMP_15 +\def (\lambda (ee: C).(match ee with [(CSort _) \Rightarrow False | (CHead _ +k _) \Rightarrow (match k with [(Bind _) \Rightarrow True | (Flat _) +\Rightarrow False])])) in (let TMP_16 \def (Flat f) in (let TMP_17 \def +(CHead c1 TMP_16 v) in (let H5 \def (eq_ind C TMP_14 TMP_15 I TMP_17 H4) in +(let TMP_18 \def (Bind b) in (let TMP_19 \def (CHead c2 TMP_18 u) in (let +TMP_20 \def (wf3 g c1 TMP_19) in (False_ind TMP_20 H5))))))))))))))))))) in +(let TMP_31 \def (\lambda (c0: C).(\lambda (c2: C).(\lambda (_: (wf3 g c0 +c2)).(\lambda (_: (((eq C c0 (CHead c1 (Flat f) v)) \to (wf3 g c1 +c2)))).(\lambda (u: T).(\lambda (_: ((\forall (t: T).((ty3 g c0 u t) \to +False)))).(\lambda (b: B).(\lambda (H4: (eq C (CHead c0 (Bind b) u) (CHead c1 +(Flat f) v))).(let TMP_22 \def (Bind b) in (let TMP_23 \def (CHead c0 TMP_22 +u) in (let TMP_24 \def (\lambda (ee: C).(match ee with [(CSort _) \Rightarrow +False | (CHead _ k _) \Rightarrow (match k with [(Bind _) \Rightarrow True | +(Flat _) \Rightarrow False])])) in (let TMP_25 \def (Flat f) in (let TMP_26 +\def (CHead c1 TMP_25 v) in (let H5 \def (eq_ind C TMP_23 TMP_24 I TMP_26 H4) +in (let TMP_27 \def (Bind Void) in (let TMP_28 \def (TSort O) in (let TMP_29 +\def (CHead c2 TMP_27 TMP_28) in (let TMP_30 \def (wf3 g c1 TMP_29) in +(False_ind TMP_30 H5))))))))))))))))))) in (let TMP_51 \def (\lambda (c0: +C).(\lambda (c2: C).(\lambda (H1: (wf3 g c0 c2)).(\lambda (H2: (((eq C c0 +(CHead c1 (Flat f) v)) \to (wf3 g c1 c2)))).(\lambda (u: T).(\lambda (f0: +F).(\lambda (H3: (eq C (CHead c0 (Flat f0) u) (CHead c1 (Flat f) v))).(let +TMP_32 \def (\lambda (e: C).(match e with [(CSort _) \Rightarrow c0 | (CHead +c _ _) \Rightarrow c])) in (let TMP_33 \def (Flat f0) in (let TMP_34 \def +(CHead c0 TMP_33 u) in (let TMP_35 \def (Flat f) in (let TMP_36 \def (CHead +c1 TMP_35 v) in (let H4 \def (f_equal C C TMP_32 TMP_34 TMP_36 H3) in (let +TMP_37 \def (\lambda (e: C).(match e with [(CSort _) \Rightarrow f0 | (CHead +_ k _) \Rightarrow (match k with [(Bind _) \Rightarrow f0 | (Flat f1) +\Rightarrow f1])])) in (let TMP_38 \def (Flat f0) in (let TMP_39 \def (CHead +c0 TMP_38 u) in (let TMP_40 \def (Flat f) in (let TMP_41 \def (CHead c1 +TMP_40 v) in (let H5 \def (f_equal C F TMP_37 TMP_39 TMP_41 H3) in (let +TMP_42 \def (\lambda (e: C).(match e with [(CSort _) \Rightarrow u | (CHead _ +_ t) \Rightarrow t])) in (let TMP_43 \def (Flat f0) in (let TMP_44 \def +(CHead c0 TMP_43 u) in (let TMP_45 \def (Flat f) in (let TMP_46 \def (CHead +c1 TMP_45 v) in (let H6 \def (f_equal C T TMP_42 TMP_44 TMP_46 H3) in (let +TMP_49 \def (\lambda (_: (eq F f0 f)).(\lambda (H8: (eq C c0 c1)).(let TMP_47 +\def (\lambda (c: C).((eq C c (CHead c1 (Flat f) v)) \to (wf3 g c1 c2))) in +(let H9 \def (eq_ind C c0 TMP_47 H2 c1 H8) in (let TMP_48 \def (\lambda (c: +C).(wf3 g c c2)) in (let H10 \def (eq_ind C c0 TMP_48 H1 c1 H8) in H10)))))) +in (let TMP_50 \def (TMP_49 H5) in (TMP_50 H4)))))))))))))))))))))))))))) in +(wf3_ind g TMP_5 TMP_12 TMP_21 TMP_31 TMP_51 y x H0)))))))) in (insert_eq C +TMP_2 TMP_3 TMP_4 TMP_52 H))))))))))). theorem wf3_gen_head2: \forall (g: G).(\forall (x: C).(\forall (c: C).(\forall (v: T).(\forall (k: K).((wf3 g x (CHead c k v)) \to (ex B (\lambda (b: B).(eq K k (Bind b))))))))) \def \lambda (g: G).(\lambda (x: C).(\lambda (c: C).(\lambda (v: T).(\lambda (k: -K).(\lambda (H: (wf3 g x (CHead c k v))).(insert_eq C (CHead c k v) (\lambda -(c0: C).(wf3 g x c0)) (\lambda (_: C).(ex B (\lambda (b: B).(eq K k (Bind -b))))) (\lambda (y: C).(\lambda (H0: (wf3 g x y)).(wf3_ind g (\lambda (_: -C).(\lambda (c1: C).((eq C c1 (CHead c k v)) \to (ex B (\lambda (b: B).(eq K -k (Bind b))))))) (\lambda (m: nat).(\lambda (H1: (eq C (CSort m) (CHead c k -v))).(let H2 \def (eq_ind C (CSort m) (\lambda (ee: C).(match ee in C return -(\lambda (_: C).Prop) with [(CSort _) \Rightarrow True | (CHead _ _ _) -\Rightarrow False])) I (CHead c k v) H1) in (False_ind (ex B (\lambda (b: -B).(eq K k (Bind b)))) H2)))) (\lambda (c1: C).(\lambda (c2: C).(\lambda (H1: -(wf3 g c1 c2)).(\lambda (H2: (((eq C c2 (CHead c k v)) \to (ex B (\lambda (b: -B).(eq K k (Bind b))))))).(\lambda (u: T).(\lambda (t: T).(\lambda (H3: (ty3 -g c1 u t)).(\lambda (b: B).(\lambda (H4: (eq C (CHead c2 (Bind b) u) (CHead c -k v))).(let H5 \def (f_equal C C (\lambda (e: C).(match e in C return -(\lambda (_: C).C) with [(CSort _) \Rightarrow c2 | (CHead c0 _ _) -\Rightarrow c0])) (CHead c2 (Bind b) u) (CHead c k v) H4) in ((let H6 \def -(f_equal C K (\lambda (e: C).(match e in C return (\lambda (_: C).K) with -[(CSort _) \Rightarrow (Bind b) | (CHead _ k0 _) \Rightarrow k0])) (CHead c2 -(Bind b) u) (CHead c k v) H4) in ((let H7 \def (f_equal C T (\lambda (e: -C).(match e in C return (\lambda (_: C).T) with [(CSort _) \Rightarrow u | -(CHead _ _ t0) \Rightarrow t0])) (CHead c2 (Bind b) u) (CHead c k v) H4) in -(\lambda (H8: (eq K (Bind b) k)).(\lambda (H9: (eq C c2 c)).(let H10 \def -(eq_ind T u (\lambda (t0: T).(ty3 g c1 t0 t)) H3 v H7) in (let H11 \def -(eq_ind C c2 (\lambda (c0: C).((eq C c0 (CHead c k v)) \to (ex B (\lambda -(b0: B).(eq K k (Bind b0)))))) H2 c H9) in (let H12 \def (eq_ind C c2 -(\lambda (c0: C).(wf3 g c1 c0)) H1 c H9) in (let H13 \def (eq_ind_r K k -(\lambda (k0: K).((eq C c (CHead c k0 v)) \to (ex B (\lambda (b0: B).(eq K k0 -(Bind b0)))))) H11 (Bind b) H8) in (eq_ind K (Bind b) (\lambda (k0: K).(ex B -(\lambda (b0: B).(eq K k0 (Bind b0))))) (ex_intro B (\lambda (b0: B).(eq K -(Bind b) (Bind b0))) b (refl_equal K (Bind b))) k H8)))))))) H6)) -H5))))))))))) (\lambda (c1: C).(\lambda (c2: C).(\lambda (H1: (wf3 g c1 -c2)).(\lambda (H2: (((eq C c2 (CHead c k v)) \to (ex B (\lambda (b: B).(eq K -k (Bind b))))))).(\lambda (u: T).(\lambda (_: ((\forall (t: T).((ty3 g c1 u -t) \to False)))).(\lambda (_: B).(\lambda (H4: (eq C (CHead c2 (Bind Void) -(TSort O)) (CHead c k v))).(let H5 \def (f_equal C C (\lambda (e: C).(match e -in C return (\lambda (_: C).C) with [(CSort _) \Rightarrow c2 | (CHead c0 _ -_) \Rightarrow c0])) (CHead c2 (Bind Void) (TSort O)) (CHead c k v) H4) in -((let H6 \def (f_equal C K (\lambda (e: C).(match e in C return (\lambda (_: -C).K) with [(CSort _) \Rightarrow (Bind Void) | (CHead _ k0 _) \Rightarrow -k0])) (CHead c2 (Bind Void) (TSort O)) (CHead c k v) H4) in ((let H7 \def -(f_equal C T (\lambda (e: C).(match e in C return (\lambda (_: C).T) with -[(CSort _) \Rightarrow (TSort O) | (CHead _ _ t) \Rightarrow t])) (CHead c2 -(Bind Void) (TSort O)) (CHead c k v) H4) in (\lambda (H8: (eq K (Bind Void) -k)).(\lambda (H9: (eq C c2 c)).(let H10 \def (eq_ind C c2 (\lambda (c0: -C).((eq C c0 (CHead c k v)) \to (ex B (\lambda (b0: B).(eq K k (Bind b0)))))) -H2 c H9) in (let H11 \def (eq_ind C c2 (\lambda (c0: C).(wf3 g c1 c0)) H1 c -H9) in (let H12 \def (eq_ind_r K k (\lambda (k0: K).((eq C c (CHead c k0 v)) -\to (ex B (\lambda (b0: B).(eq K k0 (Bind b0)))))) H10 (Bind Void) H8) in -(eq_ind K (Bind Void) (\lambda (k0: K).(ex B (\lambda (b0: B).(eq K k0 (Bind -b0))))) (let H13 \def (eq_ind_r T v (\lambda (t: T).((eq C c (CHead c (Bind -Void) t)) \to (ex B (\lambda (b0: B).(eq K (Bind Void) (Bind b0)))))) H12 -(TSort O) H7) in (ex_intro B (\lambda (b0: B).(eq K (Bind Void) (Bind b0))) -Void (refl_equal K (Bind Void)))) k H8))))))) H6)) H5)))))))))) (\lambda (c1: +K).(\lambda (H: (wf3 g x (CHead c k v))).(let TMP_1 \def (CHead c k v) in +(let TMP_2 \def (\lambda (c0: C).(wf3 g x c0)) in (let TMP_5 \def (\lambda +(_: C).(let TMP_4 \def (\lambda (b: B).(let TMP_3 \def (Bind b) in (eq K k +TMP_3))) in (ex B TMP_4))) in (let TMP_102 \def (\lambda (y: C).(\lambda (H0: +(wf3 g x y)).(let TMP_8 \def (\lambda (_: C).(\lambda (c1: C).((eq C c1 +(CHead c k v)) \to (let TMP_7 \def (\lambda (b: B).(let TMP_6 \def (Bind b) +in (eq K k TMP_6))) in (ex B TMP_7))))) in (let TMP_15 \def (\lambda (m: +nat).(\lambda (H1: (eq C (CSort m) (CHead c k v))).(let TMP_9 \def (CSort m) +in (let TMP_10 \def (\lambda (ee: C).(match ee with [(CSort _) \Rightarrow +True | (CHead _ _ _) \Rightarrow False])) in (let TMP_11 \def (CHead c k v) +in (let H2 \def (eq_ind C TMP_9 TMP_10 I TMP_11 H1) in (let TMP_13 \def +(\lambda (b: B).(let TMP_12 \def (Bind b) in (eq K k TMP_12))) in (let TMP_14 +\def (ex B TMP_13) in (False_ind TMP_14 H2))))))))) in (let TMP_49 \def +(\lambda (c1: C).(\lambda (c2: C).(\lambda (H1: (wf3 g c1 c2)).(\lambda (H2: +(((eq C c2 (CHead c k v)) \to (ex B (\lambda (b: B).(eq K k (Bind +b))))))).(\lambda (u: T).(\lambda (t: T).(\lambda (H3: (ty3 g c1 u +t)).(\lambda (b: B).(\lambda (H4: (eq C (CHead c2 (Bind b) u) (CHead c k +v))).(let TMP_16 \def (\lambda (e: C).(match e with [(CSort _) \Rightarrow c2 +| (CHead c0 _ _) \Rightarrow c0])) in (let TMP_17 \def (Bind b) in (let +TMP_18 \def (CHead c2 TMP_17 u) in (let TMP_19 \def (CHead c k v) in (let H5 +\def (f_equal C C TMP_16 TMP_18 TMP_19 H4) in (let TMP_20 \def (\lambda (e: +C).(match e with [(CSort _) \Rightarrow (Bind b) | (CHead _ k0 _) \Rightarrow +k0])) in (let TMP_21 \def (Bind b) in (let TMP_22 \def (CHead c2 TMP_21 u) in +(let TMP_23 \def (CHead c k v) in (let H6 \def (f_equal C K TMP_20 TMP_22 +TMP_23 H4) in (let TMP_24 \def (\lambda (e: C).(match e with [(CSort _) +\Rightarrow u | (CHead _ _ t0) \Rightarrow t0])) in (let TMP_25 \def (Bind b) +in (let TMP_26 \def (CHead c2 TMP_25 u) in (let TMP_27 \def (CHead c k v) in +(let H7 \def (f_equal C T TMP_24 TMP_26 TMP_27 H4) in (let TMP_47 \def +(\lambda (H8: (eq K (Bind b) k)).(\lambda (H9: (eq C c2 c)).(let TMP_28 \def +(\lambda (t0: T).(ty3 g c1 t0 t)) in (let H10 \def (eq_ind T u TMP_28 H3 v +H7) in (let TMP_31 \def (\lambda (c0: C).((eq C c0 (CHead c k v)) \to (let +TMP_30 \def (\lambda (b0: B).(let TMP_29 \def (Bind b0) in (eq K k TMP_29))) +in (ex B TMP_30)))) in (let H11 \def (eq_ind C c2 TMP_31 H2 c H9) in (let +TMP_32 \def (\lambda (c0: C).(wf3 g c1 c0)) in (let H12 \def (eq_ind C c2 +TMP_32 H1 c H9) in (let TMP_35 \def (\lambda (k0: K).((eq C c (CHead c k0 v)) +\to (let TMP_34 \def (\lambda (b0: B).(let TMP_33 \def (Bind b0) in (eq K k0 +TMP_33))) in (ex B TMP_34)))) in (let TMP_36 \def (Bind b) in (let H13 \def +(eq_ind_r K k TMP_35 H11 TMP_36 H8) in (let TMP_37 \def (Bind b) in (let +TMP_40 \def (\lambda (k0: K).(let TMP_39 \def (\lambda (b0: B).(let TMP_38 +\def (Bind b0) in (eq K k0 TMP_38))) in (ex B TMP_39))) in (let TMP_43 \def +(\lambda (b0: B).(let TMP_41 \def (Bind b) in (let TMP_42 \def (Bind b0) in +(eq K TMP_41 TMP_42)))) in (let TMP_44 \def (Bind b) in (let TMP_45 \def +(refl_equal K TMP_44) in (let TMP_46 \def (ex_intro B TMP_43 b TMP_45) in +(eq_ind K TMP_37 TMP_40 TMP_46 k H8)))))))))))))))))) in (let TMP_48 \def +(TMP_47 H6) in (TMP_48 H5))))))))))))))))))))))))))) in (let TMP_90 \def +(\lambda (c1: C).(\lambda (c2: C).(\lambda (H1: (wf3 g c1 c2)).(\lambda (H2: +(((eq C c2 (CHead c k v)) \to (ex B (\lambda (b: B).(eq K k (Bind +b))))))).(\lambda (u: T).(\lambda (_: ((\forall (t: T).((ty3 g c1 u t) \to +False)))).(\lambda (_: B).(\lambda (H4: (eq C (CHead c2 (Bind Void) (TSort +O)) (CHead c k v))).(let TMP_50 \def (\lambda (e: C).(match e with [(CSort _) +\Rightarrow c2 | (CHead c0 _ _) \Rightarrow c0])) in (let TMP_51 \def (Bind +Void) in (let TMP_52 \def (TSort O) in (let TMP_53 \def (CHead c2 TMP_51 +TMP_52) in (let TMP_54 \def (CHead c k v) in (let H5 \def (f_equal C C TMP_50 +TMP_53 TMP_54 H4) in (let TMP_55 \def (\lambda (e: C).(match e with [(CSort +_) \Rightarrow (Bind Void) | (CHead _ k0 _) \Rightarrow k0])) in (let TMP_56 +\def (Bind Void) in (let TMP_57 \def (TSort O) in (let TMP_58 \def (CHead c2 +TMP_56 TMP_57) in (let TMP_59 \def (CHead c k v) in (let H6 \def (f_equal C K +TMP_55 TMP_58 TMP_59 H4) in (let TMP_60 \def (\lambda (e: C).(match e with +[(CSort _) \Rightarrow (TSort O) | (CHead _ _ t) \Rightarrow t])) in (let +TMP_61 \def (Bind Void) in (let TMP_62 \def (TSort O) in (let TMP_63 \def +(CHead c2 TMP_61 TMP_62) in (let TMP_64 \def (CHead c k v) in (let H7 \def +(f_equal C T TMP_60 TMP_63 TMP_64 H4) in (let TMP_88 \def (\lambda (H8: (eq K +(Bind Void) k)).(\lambda (H9: (eq C c2 c)).(let TMP_67 \def (\lambda (c0: +C).((eq C c0 (CHead c k v)) \to (let TMP_66 \def (\lambda (b0: B).(let TMP_65 +\def (Bind b0) in (eq K k TMP_65))) in (ex B TMP_66)))) in (let H10 \def +(eq_ind C c2 TMP_67 H2 c H9) in (let TMP_68 \def (\lambda (c0: C).(wf3 g c1 +c0)) in (let H11 \def (eq_ind C c2 TMP_68 H1 c H9) in (let TMP_71 \def +(\lambda (k0: K).((eq C c (CHead c k0 v)) \to (let TMP_70 \def (\lambda (b0: +B).(let TMP_69 \def (Bind b0) in (eq K k0 TMP_69))) in (ex B TMP_70)))) in +(let TMP_72 \def (Bind Void) in (let H12 \def (eq_ind_r K k TMP_71 H10 TMP_72 +H8) in (let TMP_73 \def (Bind Void) in (let TMP_76 \def (\lambda (k0: K).(let +TMP_75 \def (\lambda (b0: B).(let TMP_74 \def (Bind b0) in (eq K k0 TMP_74))) +in (ex B TMP_75))) in (let TMP_80 \def (\lambda (t: T).((eq C c (CHead c +(Bind Void) t)) \to (let TMP_79 \def (\lambda (b0: B).(let TMP_77 \def (Bind +Void) in (let TMP_78 \def (Bind b0) in (eq K TMP_77 TMP_78)))) in (ex B +TMP_79)))) in (let TMP_81 \def (TSort O) in (let H13 \def (eq_ind_r T v +TMP_80 H12 TMP_81 H7) in (let TMP_84 \def (\lambda (b0: B).(let TMP_82 \def +(Bind Void) in (let TMP_83 \def (Bind b0) in (eq K TMP_82 TMP_83)))) in (let +TMP_85 \def (Bind Void) in (let TMP_86 \def (refl_equal K TMP_85) in (let +TMP_87 \def (ex_intro B TMP_84 Void TMP_86) in (eq_ind K TMP_73 TMP_76 TMP_87 +k H8))))))))))))))))))) in (let TMP_89 \def (TMP_88 H6) in (TMP_89 +H5))))))))))))))))))))))))))))) in (let TMP_101 \def (\lambda (c1: C).(\lambda (c2: C).(\lambda (H1: (wf3 g c1 c2)).(\lambda (H2: (((eq C c2 (CHead c k v)) \to (ex B (\lambda (b: B).(eq K k (Bind b))))))).(\lambda (_: -T).(\lambda (_: F).(\lambda (H3: (eq C c2 (CHead c k v))).(let H4 \def -(f_equal C C (\lambda (e: C).e) c2 (CHead c k v) H3) in (let H5 \def (eq_ind -C c2 (\lambda (c0: C).((eq C c0 (CHead c k v)) \to (ex B (\lambda (b: B).(eq -K k (Bind b)))))) H2 (CHead c k v) H4) in (let H6 \def (eq_ind C c2 (\lambda -(c0: C).(wf3 g c1 c0)) H1 (CHead c k v) H4) in (H5 (refl_equal C (CHead c k -v))))))))))))) x y H0))) H)))))). -(* COMMENTS -Initial nodes: 1225 -END *) +T).(\lambda (_: F).(\lambda (H3: (eq C c2 (CHead c k v))).(let TMP_91 \def +(\lambda (e: C).e) in (let TMP_92 \def (CHead c k v) in (let H4 \def (f_equal +C C TMP_91 c2 TMP_92 H3) in (let TMP_95 \def (\lambda (c0: C).((eq C c0 +(CHead c k v)) \to (let TMP_94 \def (\lambda (b: B).(let TMP_93 \def (Bind b) +in (eq K k TMP_93))) in (ex B TMP_94)))) in (let TMP_96 \def (CHead c k v) in +(let H5 \def (eq_ind C c2 TMP_95 H2 TMP_96 H4) in (let TMP_97 \def (\lambda +(c0: C).(wf3 g c1 c0)) in (let TMP_98 \def (CHead c k v) in (let H6 \def +(eq_ind C c2 TMP_97 H1 TMP_98 H4) in (let TMP_99 \def (CHead c k v) in (let +TMP_100 \def (refl_equal C TMP_99) in (H5 TMP_100))))))))))))))))))) in +(wf3_ind g TMP_8 TMP_15 TMP_49 TMP_90 TMP_101 x y H0)))))))) in (insert_eq C +TMP_1 TMP_2 TMP_5 TMP_102 H)))))))))). + +theorem wf3_mono: + \forall (g: G).(\forall (c: C).(\forall (c1: C).((wf3 g c c1) \to (\forall +(c2: C).((wf3 g c c2) \to (eq C c1 c2)))))) +\def + \lambda (g: G).(\lambda (c: C).(\lambda (c1: C).(\lambda (H: (wf3 g c +c1)).(let TMP_1 \def (\lambda (c0: C).(\lambda (c2: C).(\forall (c3: C).((wf3 +g c0 c3) \to (eq C c2 c3))))) in (let TMP_7 \def (\lambda (m: nat).(\lambda +(c2: C).(\lambda (H0: (wf3 g (CSort m) c2)).(let H_y \def (wf3_gen_sort1 g c2 +m H0) in (let TMP_2 \def (CSort m) in (let TMP_4 \def (\lambda (c0: C).(let +TMP_3 \def (CSort m) in (eq C TMP_3 c0))) in (let TMP_5 \def (CSort m) in +(let TMP_6 \def (refl_equal C TMP_5) in (eq_ind_r C TMP_2 TMP_4 TMP_6 c2 +H_y))))))))) in (let TMP_70 \def (\lambda (c2: C).(\lambda (c3: C).(\lambda +(_: (wf3 g c2 c3)).(\lambda (H1: ((\forall (c4: C).((wf3 g c2 c4) \to (eq C +c3 c4))))).(\lambda (u: T).(\lambda (t: T).(\lambda (H2: (ty3 g c2 u +t)).(\lambda (b: B).(\lambda (c0: C).(\lambda (H3: (wf3 g (CHead c2 (Bind b) +u) c0)).(let H_x \def (wf3_gen_bind1 g c2 c0 u b H3) in (let H4 \def H_x in +(let TMP_10 \def (\lambda (c4: C).(\lambda (_: T).(let TMP_8 \def (Bind b) in +(let TMP_9 \def (CHead c4 TMP_8 u) in (eq C c0 TMP_9))))) in (let TMP_11 \def +(\lambda (c4: C).(\lambda (_: T).(wf3 g c2 c4))) in (let TMP_12 \def (\lambda +(_: C).(\lambda (w: T).(ty3 g c2 u w))) in (let TMP_13 \def (ex3_2 C T TMP_10 +TMP_11 TMP_12) in (let TMP_17 \def (\lambda (c4: C).(let TMP_14 \def (Bind +Void) in (let TMP_15 \def (TSort O) in (let TMP_16 \def (CHead c4 TMP_14 +TMP_15) in (eq C c0 TMP_16))))) in (let TMP_18 \def (\lambda (c4: C).(wf3 g +c2 c4)) in (let TMP_19 \def (\lambda (_: C).(\forall (w: T).((ty3 g c2 u w) +\to False))) in (let TMP_20 \def (ex3 C TMP_17 TMP_18 TMP_19) in (let TMP_21 +\def (Bind b) in (let TMP_22 \def (CHead c3 TMP_21 u) in (let TMP_23 \def (eq +C TMP_22 c0) in (let TMP_45 \def (\lambda (H5: (ex3_2 C T (\lambda (c4: +C).(\lambda (_: T).(eq C c0 (CHead c4 (Bind b) u)))) (\lambda (c4: +C).(\lambda (_: T).(wf3 g c2 c4))) (\lambda (_: C).(\lambda (w: T).(ty3 g c2 +u w))))).(let TMP_26 \def (\lambda (c4: C).(\lambda (_: T).(let TMP_24 \def +(Bind b) in (let TMP_25 \def (CHead c4 TMP_24 u) in (eq C c0 TMP_25))))) in +(let TMP_27 \def (\lambda (c4: C).(\lambda (_: T).(wf3 g c2 c4))) in (let +TMP_28 \def (\lambda (_: C).(\lambda (w: T).(ty3 g c2 u w))) in (let TMP_29 +\def (Bind b) in (let TMP_30 \def (CHead c3 TMP_29 u) in (let TMP_31 \def (eq +C TMP_30 c0) in (let TMP_44 \def (\lambda (x0: C).(\lambda (x1: T).(\lambda +(H6: (eq C c0 (CHead x0 (Bind b) u))).(\lambda (H7: (wf3 g c2 x0)).(\lambda +(_: (ty3 g c2 u x1)).(let TMP_32 \def (Bind b) in (let TMP_33 \def (CHead x0 +TMP_32 u) in (let TMP_36 \def (\lambda (c4: C).(let TMP_34 \def (Bind b) in +(let TMP_35 \def (CHead c3 TMP_34 u) in (eq C TMP_35 c4)))) in (let TMP_37 +\def (Bind b) in (let TMP_38 \def (Bind b) in (let TMP_39 \def (H1 x0 H7) in +(let TMP_40 \def (Bind b) in (let TMP_41 \def (refl_equal K TMP_40) in (let +TMP_42 \def (refl_equal T u) in (let TMP_43 \def (f_equal3 C K T C CHead c3 +x0 TMP_37 TMP_38 u u TMP_39 TMP_41 TMP_42) in (eq_ind_r C TMP_33 TMP_36 +TMP_43 c0 H6)))))))))))))))) in (ex3_2_ind C T TMP_26 TMP_27 TMP_28 TMP_31 +TMP_44 H5))))))))) in (let TMP_69 \def (\lambda (H5: (ex3 C (\lambda (c4: +C).(eq C c0 (CHead c4 (Bind Void) (TSort O)))) (\lambda (c4: C).(wf3 g c2 +c4)) (\lambda (_: C).(\forall (w: T).((ty3 g c2 u w) \to False))))).(let +TMP_49 \def (\lambda (c4: C).(let TMP_46 \def (Bind Void) in (let TMP_47 \def +(TSort O) in (let TMP_48 \def (CHead c4 TMP_46 TMP_47) in (eq C c0 +TMP_48))))) in (let TMP_50 \def (\lambda (c4: C).(wf3 g c2 c4)) in (let +TMP_51 \def (\lambda (_: C).(\forall (w: T).((ty3 g c2 u w) \to False))) in +(let TMP_52 \def (Bind b) in (let TMP_53 \def (CHead c3 TMP_52 u) in (let +TMP_54 \def (eq C TMP_53 c0) in (let TMP_68 \def (\lambda (x0: C).(\lambda +(H6: (eq C c0 (CHead x0 (Bind Void) (TSort O)))).(\lambda (_: (wf3 g c2 +x0)).(\lambda (H8: ((\forall (w: T).((ty3 g c2 u w) \to False)))).(let TMP_55 +\def (Bind Void) in (let TMP_56 \def (TSort O) in (let TMP_57 \def (CHead x0 +TMP_55 TMP_56) in (let TMP_60 \def (\lambda (c4: C).(let TMP_58 \def (Bind b) +in (let TMP_59 \def (CHead c3 TMP_58 u) in (eq C TMP_59 c4)))) in (let H_x0 +\def (H8 t H2) in (let H9 \def H_x0 in (let TMP_61 \def (Bind b) in (let +TMP_62 \def (CHead c3 TMP_61 u) in (let TMP_63 \def (Bind Void) in (let +TMP_64 \def (TSort O) in (let TMP_65 \def (CHead x0 TMP_63 TMP_64) in (let +TMP_66 \def (eq C TMP_62 TMP_65) in (let TMP_67 \def (False_ind TMP_66 H9) in +(eq_ind_r C TMP_57 TMP_60 TMP_67 c0 H6)))))))))))))))))) in (ex3_ind C TMP_49 +TMP_50 TMP_51 TMP_54 TMP_68 H5))))))))) in (or_ind TMP_13 TMP_20 TMP_23 +TMP_45 TMP_69 H4)))))))))))))))))))))))))) in (let TMP_141 \def (\lambda (c2: +C).(\lambda (c3: C).(\lambda (_: (wf3 g c2 c3)).(\lambda (H1: ((\forall (c4: +C).((wf3 g c2 c4) \to (eq C c3 c4))))).(\lambda (u: T).(\lambda (H2: +((\forall (t: T).((ty3 g c2 u t) \to False)))).(\lambda (b: B).(\lambda (c0: +C).(\lambda (H3: (wf3 g (CHead c2 (Bind b) u) c0)).(let H_x \def +(wf3_gen_bind1 g c2 c0 u b H3) in (let H4 \def H_x in (let TMP_73 \def +(\lambda (c4: C).(\lambda (_: T).(let TMP_71 \def (Bind b) in (let TMP_72 +\def (CHead c4 TMP_71 u) in (eq C c0 TMP_72))))) in (let TMP_74 \def (\lambda +(c4: C).(\lambda (_: T).(wf3 g c2 c4))) in (let TMP_75 \def (\lambda (_: +C).(\lambda (w: T).(ty3 g c2 u w))) in (let TMP_76 \def (ex3_2 C T TMP_73 +TMP_74 TMP_75) in (let TMP_80 \def (\lambda (c4: C).(let TMP_77 \def (Bind +Void) in (let TMP_78 \def (TSort O) in (let TMP_79 \def (CHead c4 TMP_77 +TMP_78) in (eq C c0 TMP_79))))) in (let TMP_81 \def (\lambda (c4: C).(wf3 g +c2 c4)) in (let TMP_82 \def (\lambda (_: C).(\forall (w: T).((ty3 g c2 u w) +\to False))) in (let TMP_83 \def (ex3 C TMP_80 TMP_81 TMP_82) in (let TMP_84 +\def (Bind Void) in (let TMP_85 \def (TSort O) in (let TMP_86 \def (CHead c3 +TMP_84 TMP_85) in (let TMP_87 \def (eq C TMP_86 c0) in (let TMP_111 \def +(\lambda (H5: (ex3_2 C T (\lambda (c4: C).(\lambda (_: T).(eq C c0 (CHead c4 +(Bind b) u)))) (\lambda (c4: C).(\lambda (_: T).(wf3 g c2 c4))) (\lambda (_: +C).(\lambda (w: T).(ty3 g c2 u w))))).(let TMP_90 \def (\lambda (c4: +C).(\lambda (_: T).(let TMP_88 \def (Bind b) in (let TMP_89 \def (CHead c4 +TMP_88 u) in (eq C c0 TMP_89))))) in (let TMP_91 \def (\lambda (c4: +C).(\lambda (_: T).(wf3 g c2 c4))) in (let TMP_92 \def (\lambda (_: +C).(\lambda (w: T).(ty3 g c2 u w))) in (let TMP_93 \def (Bind Void) in (let +TMP_94 \def (TSort O) in (let TMP_95 \def (CHead c3 TMP_93 TMP_94) in (let +TMP_96 \def (eq C TMP_95 c0) in (let TMP_110 \def (\lambda (x0: C).(\lambda +(x1: T).(\lambda (H6: (eq C c0 (CHead x0 (Bind b) u))).(\lambda (_: (wf3 g c2 +x0)).(\lambda (H8: (ty3 g c2 u x1)).(let TMP_97 \def (Bind b) in (let TMP_98 +\def (CHead x0 TMP_97 u) in (let TMP_102 \def (\lambda (c4: C).(let TMP_99 +\def (Bind Void) in (let TMP_100 \def (TSort O) in (let TMP_101 \def (CHead +c3 TMP_99 TMP_100) in (eq C TMP_101 c4))))) in (let H_x0 \def (H2 x1 H8) in +(let H9 \def H_x0 in (let TMP_103 \def (Bind Void) in (let TMP_104 \def +(TSort O) in (let TMP_105 \def (CHead c3 TMP_103 TMP_104) in (let TMP_106 +\def (Bind b) in (let TMP_107 \def (CHead x0 TMP_106 u) in (let TMP_108 \def +(eq C TMP_105 TMP_107) in (let TMP_109 \def (False_ind TMP_108 H9) in +(eq_ind_r C TMP_98 TMP_102 TMP_109 c0 H6)))))))))))))))))) in (ex3_2_ind C T +TMP_90 TMP_91 TMP_92 TMP_96 TMP_110 H5)))))))))) in (let TMP_140 \def +(\lambda (H5: (ex3 C (\lambda (c4: C).(eq C c0 (CHead c4 (Bind Void) (TSort +O)))) (\lambda (c4: C).(wf3 g c2 c4)) (\lambda (_: C).(\forall (w: T).((ty3 g +c2 u w) \to False))))).(let TMP_115 \def (\lambda (c4: C).(let TMP_112 \def +(Bind Void) in (let TMP_113 \def (TSort O) in (let TMP_114 \def (CHead c4 +TMP_112 TMP_113) in (eq C c0 TMP_114))))) in (let TMP_116 \def (\lambda (c4: +C).(wf3 g c2 c4)) in (let TMP_117 \def (\lambda (_: C).(\forall (w: T).((ty3 +g c2 u w) \to False))) in (let TMP_118 \def (Bind Void) in (let TMP_119 \def +(TSort O) in (let TMP_120 \def (CHead c3 TMP_118 TMP_119) in (let TMP_121 +\def (eq C TMP_120 c0) in (let TMP_139 \def (\lambda (x0: C).(\lambda (H6: +(eq C c0 (CHead x0 (Bind Void) (TSort O)))).(\lambda (H7: (wf3 g c2 +x0)).(\lambda (_: ((\forall (w: T).((ty3 g c2 u w) \to False)))).(let TMP_122 +\def (Bind Void) in (let TMP_123 \def (TSort O) in (let TMP_124 \def (CHead +x0 TMP_122 TMP_123) in (let TMP_128 \def (\lambda (c4: C).(let TMP_125 \def +(Bind Void) in (let TMP_126 \def (TSort O) in (let TMP_127 \def (CHead c3 +TMP_125 TMP_126) in (eq C TMP_127 c4))))) in (let TMP_129 \def (Bind Void) in +(let TMP_130 \def (Bind Void) in (let TMP_131 \def (TSort O) in (let TMP_132 +\def (TSort O) in (let TMP_133 \def (H1 x0 H7) in (let TMP_134 \def (Bind +Void) in (let TMP_135 \def (refl_equal K TMP_134) in (let TMP_136 \def (TSort +O) in (let TMP_137 \def (refl_equal T TMP_136) in (let TMP_138 \def (f_equal3 +C K T C CHead c3 x0 TMP_129 TMP_130 TMP_131 TMP_132 TMP_133 TMP_135 TMP_137) +in (eq_ind_r C TMP_124 TMP_128 TMP_138 c0 H6))))))))))))))))))) in (ex3_ind C +TMP_115 TMP_116 TMP_117 TMP_121 TMP_139 H5)))))))))) in (or_ind TMP_76 TMP_83 +TMP_87 TMP_111 TMP_140 H4)))))))))))))))))))))))))) in (let TMP_142 \def +(\lambda (c2: C).(\lambda (c3: C).(\lambda (_: (wf3 g c2 c3)).(\lambda (H1: +((\forall (c4: C).((wf3 g c2 c4) \to (eq C c3 c4))))).(\lambda (u: +T).(\lambda (f: F).(\lambda (c0: C).(\lambda (H2: (wf3 g (CHead c2 (Flat f) +u) c0)).(let H_y \def (wf3_gen_flat1 g c2 c0 u f H2) in (H1 c0 H_y)))))))))) +in (wf3_ind g TMP_1 TMP_7 TMP_70 TMP_141 TMP_142 c c1 H))))))))). diff --git a/matita/matita/contribs/lambdadelta/basic_1/wf3/getl.ma b/matita/matita/contribs/lambdadelta/basic_1/wf3/getl.ma index 8a8f13780..d73b1f276 100644 --- a/matita/matita/contribs/lambdadelta/basic_1/wf3/getl.ma +++ b/matita/matita/contribs/lambdadelta/basic_1/wf3/getl.ma @@ -14,9 +14,9 @@ (* This file was automatically generated: do not edit *********************) -include "Basic-1/wf3/clear.ma". +include "basic_1/wf3/clear.ma". -include "Basic-1/ty3/dec.ma". +include "basic_1/ty3/dec.ma". theorem wf3_getl_conf: \forall (b: B).(\forall (i: nat).(\forall (c1: C).(\forall (d1: C).(\forall @@ -25,181 +25,302 @@ C).((wf3 g c1 c2) \to (\forall (w: T).((ty3 g d1 v w) \to (ex2 C (\lambda (d2: C).(getl i c2 (CHead d2 (Bind b) v))) (\lambda (d2: C).(wf3 g d1 d2))))))))))))) \def - \lambda (b: B).(\lambda (i: nat).(nat_ind (\lambda (n: nat).(\forall (c1: -C).(\forall (d1: C).(\forall (v: T).((getl n c1 (CHead d1 (Bind b) v)) \to -(\forall (g: G).(\forall (c2: C).((wf3 g c1 c2) \to (\forall (w: T).((ty3 g -d1 v w) \to (ex2 C (\lambda (d2: C).(getl n c2 (CHead d2 (Bind b) v))) -(\lambda (d2: C).(wf3 g d1 d2))))))))))))) (\lambda (c1: C).(\lambda (d1: -C).(\lambda (v: T).(\lambda (H: (getl O c1 (CHead d1 (Bind b) v))).(\lambda -(g: G).(\lambda (c2: C).(\lambda (H0: (wf3 g c1 c2)).(\lambda (w: T).(\lambda -(H1: (ty3 g d1 v w)).(let H_y \def (wf3_clear_conf c1 (CHead d1 (Bind b) v) -(getl_gen_O c1 (CHead d1 (Bind b) v) H) g c2 H0) in (let H_x \def -(wf3_gen_bind1 g d1 c2 v b H_y) in (let H2 \def H_x in (or_ind (ex3_2 C T -(\lambda (c3: C).(\lambda (_: T).(eq C c2 (CHead c3 (Bind b) v)))) (\lambda -(c3: C).(\lambda (_: T).(wf3 g d1 c3))) (\lambda (_: C).(\lambda (w0: T).(ty3 -g d1 v w0)))) (ex3 C (\lambda (c3: C).(eq C c2 (CHead c3 (Bind Void) (TSort -O)))) (\lambda (c3: C).(wf3 g d1 c3)) (\lambda (_: C).(\forall (w0: T).((ty3 -g d1 v w0) \to False)))) (ex2 C (\lambda (d2: C).(getl O c2 (CHead d2 (Bind -b) v))) (\lambda (d2: C).(wf3 g d1 d2))) (\lambda (H3: (ex3_2 C T (\lambda -(c3: C).(\lambda (_: T).(eq C c2 (CHead c3 (Bind b) v)))) (\lambda (c3: -C).(\lambda (_: T).(wf3 g d1 c3))) (\lambda (_: C).(\lambda (w0: T).(ty3 g d1 -v w0))))).(ex3_2_ind C T (\lambda (c3: C).(\lambda (_: T).(eq C c2 (CHead c3 -(Bind b) v)))) (\lambda (c3: C).(\lambda (_: T).(wf3 g d1 c3))) (\lambda (_: -C).(\lambda (w0: T).(ty3 g d1 v w0))) (ex2 C (\lambda (d2: C).(getl O c2 -(CHead d2 (Bind b) v))) (\lambda (d2: C).(wf3 g d1 d2))) (\lambda (x0: + \lambda (b: B).(\lambda (i: nat).(let TMP_5 \def (\lambda (n: nat).(\forall +(c1: C).(\forall (d1: C).(\forall (v: T).((getl n c1 (CHead d1 (Bind b) v)) +\to (\forall (g: G).(\forall (c2: C).((wf3 g c1 c2) \to (\forall (w: T).((ty3 +g d1 v w) \to (let TMP_3 \def (\lambda (d2: C).(let TMP_1 \def (Bind b) in +(let TMP_2 \def (CHead d2 TMP_1 v) in (getl n c2 TMP_2)))) in (let TMP_4 \def +(\lambda (d2: C).(wf3 g d1 d2)) in (ex2 C TMP_3 TMP_4))))))))))))) in (let +TMP_86 \def (\lambda (c1: C).(\lambda (d1: C).(\lambda (v: T).(\lambda (H: +(getl O c1 (CHead d1 (Bind b) v))).(\lambda (g: G).(\lambda (c2: C).(\lambda +(H0: (wf3 g c1 c2)).(\lambda (w: T).(\lambda (H1: (ty3 g d1 v w)).(let TMP_6 +\def (Bind b) in (let TMP_7 \def (CHead d1 TMP_6 v) in (let TMP_8 \def (Bind +b) in (let TMP_9 \def (CHead d1 TMP_8 v) in (let TMP_10 \def (getl_gen_O c1 +TMP_9 H) in (let H_y \def (wf3_clear_conf c1 TMP_7 TMP_10 g c2 H0) in (let +H_x \def (wf3_gen_bind1 g d1 c2 v b H_y) in (let H2 \def H_x in (let TMP_13 +\def (\lambda (c3: C).(\lambda (_: T).(let TMP_11 \def (Bind b) in (let +TMP_12 \def (CHead c3 TMP_11 v) in (eq C c2 TMP_12))))) in (let TMP_14 \def +(\lambda (c3: C).(\lambda (_: T).(wf3 g d1 c3))) in (let TMP_15 \def (\lambda +(_: C).(\lambda (w0: T).(ty3 g d1 v w0))) in (let TMP_16 \def (ex3_2 C T +TMP_13 TMP_14 TMP_15) in (let TMP_20 \def (\lambda (c3: C).(let TMP_17 \def +(Bind Void) in (let TMP_18 \def (TSort O) in (let TMP_19 \def (CHead c3 +TMP_17 TMP_18) in (eq C c2 TMP_19))))) in (let TMP_21 \def (\lambda (c3: +C).(wf3 g d1 c3)) in (let TMP_22 \def (\lambda (_: C).(\forall (w0: T).((ty3 +g d1 v w0) \to False))) in (let TMP_23 \def (ex3 C TMP_20 TMP_21 TMP_22) in +(let TMP_26 \def (\lambda (d2: C).(let TMP_24 \def (Bind b) in (let TMP_25 +\def (CHead d2 TMP_24 v) in (getl O c2 TMP_25)))) in (let TMP_27 \def +(\lambda (d2: C).(wf3 g d1 d2)) in (let TMP_28 \def (ex2 C TMP_26 TMP_27) in +(let TMP_55 \def (\lambda (H3: (ex3_2 C T (\lambda (c3: C).(\lambda (_: +T).(eq C c2 (CHead c3 (Bind b) v)))) (\lambda (c3: C).(\lambda (_: T).(wf3 g +d1 c3))) (\lambda (_: C).(\lambda (w0: T).(ty3 g d1 v w0))))).(let TMP_31 +\def (\lambda (c3: C).(\lambda (_: T).(let TMP_29 \def (Bind b) in (let +TMP_30 \def (CHead c3 TMP_29 v) in (eq C c2 TMP_30))))) in (let TMP_32 \def +(\lambda (c3: C).(\lambda (_: T).(wf3 g d1 c3))) in (let TMP_33 \def (\lambda +(_: C).(\lambda (w0: T).(ty3 g d1 v w0))) in (let TMP_36 \def (\lambda (d2: +C).(let TMP_34 \def (Bind b) in (let TMP_35 \def (CHead d2 TMP_34 v) in (getl +O c2 TMP_35)))) in (let TMP_37 \def (\lambda (d2: C).(wf3 g d1 d2)) in (let +TMP_38 \def (ex2 C TMP_36 TMP_37) in (let TMP_54 \def (\lambda (x0: C).(\lambda (x1: T).(\lambda (H4: (eq C c2 (CHead x0 (Bind b) v))).(\lambda -(H5: (wf3 g d1 x0)).(\lambda (_: (ty3 g d1 v x1)).(eq_ind_r C (CHead x0 (Bind -b) v) (\lambda (c: C).(ex2 C (\lambda (d2: C).(getl O c (CHead d2 (Bind b) -v))) (\lambda (d2: C).(wf3 g d1 d2)))) (ex_intro2 C (\lambda (d2: C).(getl O -(CHead x0 (Bind b) v) (CHead d2 (Bind b) v))) (\lambda (d2: C).(wf3 g d1 d2)) -x0 (getl_refl b x0 v) H5) c2 H4)))))) H3)) (\lambda (H3: (ex3 C (\lambda (c3: -C).(eq C c2 (CHead c3 (Bind Void) (TSort O)))) (\lambda (c3: C).(wf3 g d1 -c3)) (\lambda (_: C).(\forall (w0: T).((ty3 g d1 v w0) \to -False))))).(ex3_ind C (\lambda (c3: C).(eq C c2 (CHead c3 (Bind Void) (TSort -O)))) (\lambda (c3: C).(wf3 g d1 c3)) (\lambda (_: C).(\forall (w0: T).((ty3 -g d1 v w0) \to False))) (ex2 C (\lambda (d2: C).(getl O c2 (CHead d2 (Bind b) -v))) (\lambda (d2: C).(wf3 g d1 d2))) (\lambda (x0: C).(\lambda (H4: (eq C c2 -(CHead x0 (Bind Void) (TSort O)))).(\lambda (_: (wf3 g d1 x0)).(\lambda (H6: -((\forall (w0: T).((ty3 g d1 v w0) \to False)))).(eq_ind_r C (CHead x0 (Bind -Void) (TSort O)) (\lambda (c: C).(ex2 C (\lambda (d2: C).(getl O c (CHead d2 -(Bind b) v))) (\lambda (d2: C).(wf3 g d1 d2)))) (let H_x0 \def (H6 w H1) in -(let H7 \def H_x0 in (False_ind (ex2 C (\lambda (d2: C).(getl O (CHead x0 -(Bind Void) (TSort O)) (CHead d2 (Bind b) v))) (\lambda (d2: C).(wf3 g d1 -d2))) H7))) c2 H4))))) H3)) H2))))))))))))) (\lambda (n: nat).(\lambda (H: -((\forall (c1: C).(\forall (d1: C).(\forall (v: T).((getl n c1 (CHead d1 -(Bind b) v)) \to (\forall (g: G).(\forall (c2: C).((wf3 g c1 c2) \to (\forall -(w: T).((ty3 g d1 v w) \to (ex2 C (\lambda (d2: C).(getl n c2 (CHead d2 (Bind -b) v))) (\lambda (d2: C).(wf3 g d1 d2)))))))))))))).(\lambda (c1: C).(C_ind -(\lambda (c: C).(\forall (d1: C).(\forall (v: T).((getl (S n) c (CHead d1 -(Bind b) v)) \to (\forall (g: G).(\forall (c2: C).((wf3 g c c2) \to (\forall -(w: T).((ty3 g d1 v w) \to (ex2 C (\lambda (d2: C).(getl (S n) c2 (CHead d2 -(Bind b) v))) (\lambda (d2: C).(wf3 g d1 d2)))))))))))) (\lambda (n0: -nat).(\lambda (d1: C).(\lambda (v: T).(\lambda (H0: (getl (S n) (CSort n0) -(CHead d1 (Bind b) v))).(\lambda (g: G).(\lambda (c2: C).(\lambda (_: (wf3 g -(CSort n0) c2)).(\lambda (w: T).(\lambda (_: (ty3 g d1 v w)).(getl_gen_sort -n0 (S n) (CHead d1 (Bind b) v) H0 (ex2 C (\lambda (d2: C).(getl (S n) c2 -(CHead d2 (Bind b) v))) (\lambda (d2: C).(wf3 g d1 d2))))))))))))) (\lambda -(c: C).(\lambda (H0: ((\forall (d1: C).(\forall (v: T).((getl (S n) c (CHead -d1 (Bind b) v)) \to (\forall (g: G).(\forall (c2: C).((wf3 g c c2) \to -(\forall (w: T).((ty3 g d1 v w) \to (ex2 C (\lambda (d2: C).(getl (S n) c2 -(CHead d2 (Bind b) v))) (\lambda (d2: C).(wf3 g d1 d2))))))))))))).(\lambda -(k: K).(\lambda (t: T).(\lambda (d1: C).(\lambda (v: T).(\lambda (H1: (getl -(S n) (CHead c k t) (CHead d1 (Bind b) v))).(\lambda (g: G).(\lambda (c2: -C).(\lambda (H2: (wf3 g (CHead c k t) c2)).(\lambda (w: T).(\lambda (H3: (ty3 -g d1 v w)).(K_ind (\lambda (k0: K).((wf3 g (CHead c k0 t) c2) \to ((getl (r -k0 n) c (CHead d1 (Bind b) v)) \to (ex2 C (\lambda (d2: C).(getl (S n) c2 -(CHead d2 (Bind b) v))) (\lambda (d2: C).(wf3 g d1 d2)))))) (\lambda (b0: -B).(\lambda (H4: (wf3 g (CHead c (Bind b0) t) c2)).(\lambda (H5: (getl (r -(Bind b0) n) c (CHead d1 (Bind b) v))).(let H_x \def (wf3_gen_bind1 g c c2 t -b0 H4) in (let H6 \def H_x in (or_ind (ex3_2 C T (\lambda (c3: C).(\lambda -(_: T).(eq C c2 (CHead c3 (Bind b0) t)))) (\lambda (c3: C).(\lambda (_: -T).(wf3 g c c3))) (\lambda (_: C).(\lambda (w0: T).(ty3 g c t w0)))) (ex3 C -(\lambda (c3: C).(eq C c2 (CHead c3 (Bind Void) (TSort O)))) (\lambda (c3: -C).(wf3 g c c3)) (\lambda (_: C).(\forall (w0: T).((ty3 g c t w0) \to -False)))) (ex2 C (\lambda (d2: C).(getl (S n) c2 (CHead d2 (Bind b) v))) -(\lambda (d2: C).(wf3 g d1 d2))) (\lambda (H7: (ex3_2 C T (\lambda (c3: -C).(\lambda (_: T).(eq C c2 (CHead c3 (Bind b0) t)))) (\lambda (c3: -C).(\lambda (_: T).(wf3 g c c3))) (\lambda (_: C).(\lambda (w0: T).(ty3 g c t -w0))))).(ex3_2_ind C T (\lambda (c3: C).(\lambda (_: T).(eq C c2 (CHead c3 -(Bind b0) t)))) (\lambda (c3: C).(\lambda (_: T).(wf3 g c c3))) (\lambda (_: -C).(\lambda (w0: T).(ty3 g c t w0))) (ex2 C (\lambda (d2: C).(getl (S n) c2 -(CHead d2 (Bind b) v))) (\lambda (d2: C).(wf3 g d1 d2))) (\lambda (x0: -C).(\lambda (x1: T).(\lambda (H8: (eq C c2 (CHead x0 (Bind b0) t))).(\lambda -(H9: (wf3 g c x0)).(\lambda (_: (ty3 g c t x1)).(eq_ind_r C (CHead x0 (Bind -b0) t) (\lambda (c0: C).(ex2 C (\lambda (d2: C).(getl (S n) c0 (CHead d2 -(Bind b) v))) (\lambda (d2: C).(wf3 g d1 d2)))) (let H_x0 \def (H c d1 v H5 g -x0 H9 w H3) in (let H11 \def H_x0 in (ex2_ind C (\lambda (d2: C).(getl n x0 -(CHead d2 (Bind b) v))) (\lambda (d2: C).(wf3 g d1 d2)) (ex2 C (\lambda (d2: -C).(getl (S n) (CHead x0 (Bind b0) t) (CHead d2 (Bind b) v))) (\lambda (d2: -C).(wf3 g d1 d2))) (\lambda (x: C).(\lambda (H12: (getl n x0 (CHead x (Bind -b) v))).(\lambda (H13: (wf3 g d1 x)).(ex_intro2 C (\lambda (d2: C).(getl (S -n) (CHead x0 (Bind b0) t) (CHead d2 (Bind b) v))) (\lambda (d2: C).(wf3 g d1 -d2)) x (getl_head (Bind b0) n x0 (CHead x (Bind b) v) H12 t) H13)))) H11))) -c2 H8)))))) H7)) (\lambda (H7: (ex3 C (\lambda (c3: C).(eq C c2 (CHead c3 -(Bind Void) (TSort O)))) (\lambda (c3: C).(wf3 g c c3)) (\lambda (_: -C).(\forall (w0: T).((ty3 g c t w0) \to False))))).(ex3_ind C (\lambda (c3: -C).(eq C c2 (CHead c3 (Bind Void) (TSort O)))) (\lambda (c3: C).(wf3 g c c3)) -(\lambda (_: C).(\forall (w0: T).((ty3 g c t w0) \to False))) (ex2 C (\lambda -(d2: C).(getl (S n) c2 (CHead d2 (Bind b) v))) (\lambda (d2: C).(wf3 g d1 -d2))) (\lambda (x0: C).(\lambda (H8: (eq C c2 (CHead x0 (Bind Void) (TSort -O)))).(\lambda (H9: (wf3 g c x0)).(\lambda (_: ((\forall (w0: T).((ty3 g c t -w0) \to False)))).(eq_ind_r C (CHead x0 (Bind Void) (TSort O)) (\lambda (c0: -C).(ex2 C (\lambda (d2: C).(getl (S n) c0 (CHead d2 (Bind b) v))) (\lambda -(d2: C).(wf3 g d1 d2)))) (let H_x0 \def (H c d1 v H5 g x0 H9 w H3) in (let -H11 \def H_x0 in (ex2_ind C (\lambda (d2: C).(getl n x0 (CHead d2 (Bind b) -v))) (\lambda (d2: C).(wf3 g d1 d2)) (ex2 C (\lambda (d2: C).(getl (S n) -(CHead x0 (Bind Void) (TSort O)) (CHead d2 (Bind b) v))) (\lambda (d2: -C).(wf3 g d1 d2))) (\lambda (x: C).(\lambda (H12: (getl n x0 (CHead x (Bind -b) v))).(\lambda (H13: (wf3 g d1 x)).(ex_intro2 C (\lambda (d2: C).(getl (S -n) (CHead x0 (Bind Void) (TSort O)) (CHead d2 (Bind b) v))) (\lambda (d2: -C).(wf3 g d1 d2)) x (getl_head (Bind Void) n x0 (CHead x (Bind b) v) H12 -(TSort O)) H13)))) H11))) c2 H8))))) H7)) H6)))))) (\lambda (f: F).(\lambda -(H4: (wf3 g (CHead c (Flat f) t) c2)).(\lambda (H5: (getl (r (Flat f) n) c -(CHead d1 (Bind b) v))).(let H_y \def (wf3_gen_flat1 g c c2 t f H4) in (H0 d1 -v H5 g c2 H_y w H3))))) k H2 (getl_gen_S k c (CHead d1 (Bind b) v) t n -H1)))))))))))))) c1)))) i)). -(* COMMENTS -Initial nodes: 2531 -END *) +(H5: (wf3 g d1 x0)).(\lambda (_: (ty3 g d1 v x1)).(let TMP_39 \def (Bind b) +in (let TMP_40 \def (CHead x0 TMP_39 v) in (let TMP_45 \def (\lambda (c: +C).(let TMP_43 \def (\lambda (d2: C).(let TMP_41 \def (Bind b) in (let TMP_42 +\def (CHead d2 TMP_41 v) in (getl O c TMP_42)))) in (let TMP_44 \def (\lambda +(d2: C).(wf3 g d1 d2)) in (ex2 C TMP_43 TMP_44)))) in (let TMP_50 \def +(\lambda (d2: C).(let TMP_46 \def (Bind b) in (let TMP_47 \def (CHead x0 +TMP_46 v) in (let TMP_48 \def (Bind b) in (let TMP_49 \def (CHead d2 TMP_48 +v) in (getl O TMP_47 TMP_49)))))) in (let TMP_51 \def (\lambda (d2: C).(wf3 g +d1 d2)) in (let TMP_52 \def (getl_refl b x0 v) in (let TMP_53 \def (ex_intro2 +C TMP_50 TMP_51 x0 TMP_52 H5) in (eq_ind_r C TMP_40 TMP_45 TMP_53 c2 +H4))))))))))))) in (ex3_2_ind C T TMP_31 TMP_32 TMP_33 TMP_38 TMP_54 +H3))))))))) in (let TMP_85 \def (\lambda (H3: (ex3 C (\lambda (c3: C).(eq C +c2 (CHead c3 (Bind Void) (TSort O)))) (\lambda (c3: C).(wf3 g d1 c3)) +(\lambda (_: C).(\forall (w0: T).((ty3 g d1 v w0) \to False))))).(let TMP_59 +\def (\lambda (c3: C).(let TMP_56 \def (Bind Void) in (let TMP_57 \def (TSort +O) in (let TMP_58 \def (CHead c3 TMP_56 TMP_57) in (eq C c2 TMP_58))))) in +(let TMP_60 \def (\lambda (c3: C).(wf3 g d1 c3)) in (let TMP_61 \def (\lambda +(_: C).(\forall (w0: T).((ty3 g d1 v w0) \to False))) in (let TMP_64 \def +(\lambda (d2: C).(let TMP_62 \def (Bind b) in (let TMP_63 \def (CHead d2 +TMP_62 v) in (getl O c2 TMP_63)))) in (let TMP_65 \def (\lambda (d2: C).(wf3 +g d1 d2)) in (let TMP_66 \def (ex2 C TMP_64 TMP_65) in (let TMP_84 \def +(\lambda (x0: C).(\lambda (H4: (eq C c2 (CHead x0 (Bind Void) (TSort +O)))).(\lambda (_: (wf3 g d1 x0)).(\lambda (H6: ((\forall (w0: T).((ty3 g d1 +v w0) \to False)))).(let TMP_67 \def (Bind Void) in (let TMP_68 \def (TSort +O) in (let TMP_69 \def (CHead x0 TMP_67 TMP_68) in (let TMP_74 \def (\lambda +(c: C).(let TMP_72 \def (\lambda (d2: C).(let TMP_70 \def (Bind b) in (let +TMP_71 \def (CHead d2 TMP_70 v) in (getl O c TMP_71)))) in (let TMP_73 \def +(\lambda (d2: C).(wf3 g d1 d2)) in (ex2 C TMP_72 TMP_73)))) in (let H_x0 \def +(H6 w H1) in (let H7 \def H_x0 in (let TMP_80 \def (\lambda (d2: C).(let +TMP_75 \def (Bind Void) in (let TMP_76 \def (TSort O) in (let TMP_77 \def +(CHead x0 TMP_75 TMP_76) in (let TMP_78 \def (Bind b) in (let TMP_79 \def +(CHead d2 TMP_78 v) in (getl O TMP_77 TMP_79))))))) in (let TMP_81 \def +(\lambda (d2: C).(wf3 g d1 d2)) in (let TMP_82 \def (ex2 C TMP_80 TMP_81) in +(let TMP_83 \def (False_ind TMP_82 H7) in (eq_ind_r C TMP_69 TMP_74 TMP_83 c2 +H4))))))))))))))) in (ex3_ind C TMP_59 TMP_60 TMP_61 TMP_66 TMP_84 +H3))))))))) in (or_ind TMP_16 TMP_23 TMP_28 TMP_55 TMP_85 +H2))))))))))))))))))))))))))))))) in (let TMP_231 \def (\lambda (n: +nat).(\lambda (H: ((\forall (c1: C).(\forall (d1: C).(\forall (v: T).((getl n +c1 (CHead d1 (Bind b) v)) \to (\forall (g: G).(\forall (c2: C).((wf3 g c1 c2) +\to (\forall (w: T).((ty3 g d1 v w) \to (ex2 C (\lambda (d2: C).(getl n c2 +(CHead d2 (Bind b) v))) (\lambda (d2: C).(wf3 g d1 d2)))))))))))))).(\lambda +(c1: C).(let TMP_92 \def (\lambda (c: C).(\forall (d1: C).(\forall (v: +T).((getl (S n) c (CHead d1 (Bind b) v)) \to (\forall (g: G).(\forall (c2: +C).((wf3 g c c2) \to (\forall (w: T).((ty3 g d1 v w) \to (let TMP_90 \def +(\lambda (d2: C).(let TMP_87 \def (S n) in (let TMP_88 \def (Bind b) in (let +TMP_89 \def (CHead d2 TMP_88 v) in (getl TMP_87 c2 TMP_89))))) in (let TMP_91 +\def (\lambda (d2: C).(wf3 g d1 d2)) in (ex2 C TMP_90 TMP_91)))))))))))) in +(let TMP_102 \def (\lambda (n0: nat).(\lambda (d1: C).(\lambda (v: +T).(\lambda (H0: (getl (S n) (CSort n0) (CHead d1 (Bind b) v))).(\lambda (g: +G).(\lambda (c2: C).(\lambda (_: (wf3 g (CSort n0) c2)).(\lambda (w: +T).(\lambda (_: (ty3 g d1 v w)).(let TMP_93 \def (S n) in (let TMP_94 \def +(Bind b) in (let TMP_95 \def (CHead d1 TMP_94 v) in (let TMP_99 \def (\lambda +(d2: C).(let TMP_96 \def (S n) in (let TMP_97 \def (Bind b) in (let TMP_98 +\def (CHead d2 TMP_97 v) in (getl TMP_96 c2 TMP_98))))) in (let TMP_100 \def +(\lambda (d2: C).(wf3 g d1 d2)) in (let TMP_101 \def (ex2 C TMP_99 TMP_100) +in (getl_gen_sort n0 TMP_93 TMP_95 H0 TMP_101)))))))))))))))) in (let TMP_230 +\def (\lambda (c: C).(\lambda (H0: ((\forall (d1: C).(\forall (v: T).((getl +(S n) c (CHead d1 (Bind b) v)) \to (\forall (g: G).(\forall (c2: C).((wf3 g c +c2) \to (\forall (w: T).((ty3 g d1 v w) \to (ex2 C (\lambda (d2: C).(getl (S +n) c2 (CHead d2 (Bind b) v))) (\lambda (d2: C).(wf3 g d1 +d2))))))))))))).(\lambda (k: K).(\lambda (t: T).(\lambda (d1: C).(\lambda (v: +T).(\lambda (H1: (getl (S n) (CHead c k t) (CHead d1 (Bind b) v))).(\lambda +(g: G).(\lambda (c2: C).(\lambda (H2: (wf3 g (CHead c k t) c2)).(\lambda (w: +T).(\lambda (H3: (ty3 g d1 v w)).(let TMP_108 \def (\lambda (k0: K).((wf3 g +(CHead c k0 t) c2) \to ((getl (r k0 n) c (CHead d1 (Bind b) v)) \to (let +TMP_106 \def (\lambda (d2: C).(let TMP_103 \def (S n) in (let TMP_104 \def +(Bind b) in (let TMP_105 \def (CHead d2 TMP_104 v) in (getl TMP_103 c2 +TMP_105))))) in (let TMP_107 \def (\lambda (d2: C).(wf3 g d1 d2)) in (ex2 C +TMP_106 TMP_107)))))) in (let TMP_225 \def (\lambda (b0: B).(\lambda (H4: +(wf3 g (CHead c (Bind b0) t) c2)).(\lambda (H5: (getl (r (Bind b0) n) c +(CHead d1 (Bind b) v))).(let H_x \def (wf3_gen_bind1 g c c2 t b0 H4) in (let +H6 \def H_x in (let TMP_111 \def (\lambda (c3: C).(\lambda (_: T).(let +TMP_109 \def (Bind b0) in (let TMP_110 \def (CHead c3 TMP_109 t) in (eq C c2 +TMP_110))))) in (let TMP_112 \def (\lambda (c3: C).(\lambda (_: T).(wf3 g c +c3))) in (let TMP_113 \def (\lambda (_: C).(\lambda (w0: T).(ty3 g c t w0))) +in (let TMP_114 \def (ex3_2 C T TMP_111 TMP_112 TMP_113) in (let TMP_118 \def +(\lambda (c3: C).(let TMP_115 \def (Bind Void) in (let TMP_116 \def (TSort O) +in (let TMP_117 \def (CHead c3 TMP_115 TMP_116) in (eq C c2 TMP_117))))) in +(let TMP_119 \def (\lambda (c3: C).(wf3 g c c3)) in (let TMP_120 \def +(\lambda (_: C).(\forall (w0: T).((ty3 g c t w0) \to False))) in (let TMP_121 +\def (ex3 C TMP_118 TMP_119 TMP_120) in (let TMP_125 \def (\lambda (d2: +C).(let TMP_122 \def (S n) in (let TMP_123 \def (Bind b) in (let TMP_124 \def +(CHead d2 TMP_123 v) in (getl TMP_122 c2 TMP_124))))) in (let TMP_126 \def +(\lambda (d2: C).(wf3 g d1 d2)) in (let TMP_127 \def (ex2 C TMP_125 TMP_126) +in (let TMP_173 \def (\lambda (H7: (ex3_2 C T (\lambda (c3: C).(\lambda (_: +T).(eq C c2 (CHead c3 (Bind b0) t)))) (\lambda (c3: C).(\lambda (_: T).(wf3 g +c c3))) (\lambda (_: C).(\lambda (w0: T).(ty3 g c t w0))))).(let TMP_130 \def +(\lambda (c3: C).(\lambda (_: T).(let TMP_128 \def (Bind b0) in (let TMP_129 +\def (CHead c3 TMP_128 t) in (eq C c2 TMP_129))))) in (let TMP_131 \def +(\lambda (c3: C).(\lambda (_: T).(wf3 g c c3))) in (let TMP_132 \def (\lambda +(_: C).(\lambda (w0: T).(ty3 g c t w0))) in (let TMP_136 \def (\lambda (d2: +C).(let TMP_133 \def (S n) in (let TMP_134 \def (Bind b) in (let TMP_135 \def +(CHead d2 TMP_134 v) in (getl TMP_133 c2 TMP_135))))) in (let TMP_137 \def +(\lambda (d2: C).(wf3 g d1 d2)) in (let TMP_138 \def (ex2 C TMP_136 TMP_137) +in (let TMP_172 \def (\lambda (x0: C).(\lambda (x1: T).(\lambda (H8: (eq C c2 +(CHead x0 (Bind b0) t))).(\lambda (H9: (wf3 g c x0)).(\lambda (_: (ty3 g c t +x1)).(let TMP_139 \def (Bind b0) in (let TMP_140 \def (CHead x0 TMP_139 t) in +(let TMP_146 \def (\lambda (c0: C).(let TMP_144 \def (\lambda (d2: C).(let +TMP_141 \def (S n) in (let TMP_142 \def (Bind b) in (let TMP_143 \def (CHead +d2 TMP_142 v) in (getl TMP_141 c0 TMP_143))))) in (let TMP_145 \def (\lambda +(d2: C).(wf3 g d1 d2)) in (ex2 C TMP_144 TMP_145)))) in (let H_x0 \def (H c +d1 v H5 g x0 H9 w H3) in (let H11 \def H_x0 in (let TMP_149 \def (\lambda +(d2: C).(let TMP_147 \def (Bind b) in (let TMP_148 \def (CHead d2 TMP_147 v) +in (getl n x0 TMP_148)))) in (let TMP_150 \def (\lambda (d2: C).(wf3 g d1 +d2)) in (let TMP_156 \def (\lambda (d2: C).(let TMP_151 \def (S n) in (let +TMP_152 \def (Bind b0) in (let TMP_153 \def (CHead x0 TMP_152 t) in (let +TMP_154 \def (Bind b) in (let TMP_155 \def (CHead d2 TMP_154 v) in (getl +TMP_151 TMP_153 TMP_155))))))) in (let TMP_157 \def (\lambda (d2: C).(wf3 g +d1 d2)) in (let TMP_158 \def (ex2 C TMP_156 TMP_157) in (let TMP_170 \def +(\lambda (x: C).(\lambda (H12: (getl n x0 (CHead x (Bind b) v))).(\lambda +(H13: (wf3 g d1 x)).(let TMP_164 \def (\lambda (d2: C).(let TMP_159 \def (S +n) in (let TMP_160 \def (Bind b0) in (let TMP_161 \def (CHead x0 TMP_160 t) +in (let TMP_162 \def (Bind b) in (let TMP_163 \def (CHead d2 TMP_162 v) in +(getl TMP_159 TMP_161 TMP_163))))))) in (let TMP_165 \def (\lambda (d2: +C).(wf3 g d1 d2)) in (let TMP_166 \def (Bind b0) in (let TMP_167 \def (Bind +b) in (let TMP_168 \def (CHead x TMP_167 v) in (let TMP_169 \def (getl_head +TMP_166 n x0 TMP_168 H12 t) in (ex_intro2 C TMP_164 TMP_165 x TMP_169 +H13)))))))))) in (let TMP_171 \def (ex2_ind C TMP_149 TMP_150 TMP_158 TMP_170 +H11) in (eq_ind_r C TMP_140 TMP_146 TMP_171 c2 H8)))))))))))))))))) in +(ex3_2_ind C T TMP_130 TMP_131 TMP_132 TMP_138 TMP_172 H7))))))))) in (let +TMP_224 \def (\lambda (H7: (ex3 C (\lambda (c3: C).(eq C c2 (CHead c3 (Bind +Void) (TSort O)))) (\lambda (c3: C).(wf3 g c c3)) (\lambda (_: C).(\forall +(w0: T).((ty3 g c t w0) \to False))))).(let TMP_177 \def (\lambda (c3: +C).(let TMP_174 \def (Bind Void) in (let TMP_175 \def (TSort O) in (let +TMP_176 \def (CHead c3 TMP_174 TMP_175) in (eq C c2 TMP_176))))) in (let +TMP_178 \def (\lambda (c3: C).(wf3 g c c3)) in (let TMP_179 \def (\lambda (_: +C).(\forall (w0: T).((ty3 g c t w0) \to False))) in (let TMP_183 \def +(\lambda (d2: C).(let TMP_180 \def (S n) in (let TMP_181 \def (Bind b) in +(let TMP_182 \def (CHead d2 TMP_181 v) in (getl TMP_180 c2 TMP_182))))) in +(let TMP_184 \def (\lambda (d2: C).(wf3 g d1 d2)) in (let TMP_185 \def (ex2 C +TMP_183 TMP_184) in (let TMP_223 \def (\lambda (x0: C).(\lambda (H8: (eq C c2 +(CHead x0 (Bind Void) (TSort O)))).(\lambda (H9: (wf3 g c x0)).(\lambda (_: +((\forall (w0: T).((ty3 g c t w0) \to False)))).(let TMP_186 \def (Bind Void) +in (let TMP_187 \def (TSort O) in (let TMP_188 \def (CHead x0 TMP_186 +TMP_187) in (let TMP_194 \def (\lambda (c0: C).(let TMP_192 \def (\lambda +(d2: C).(let TMP_189 \def (S n) in (let TMP_190 \def (Bind b) in (let TMP_191 +\def (CHead d2 TMP_190 v) in (getl TMP_189 c0 TMP_191))))) in (let TMP_193 +\def (\lambda (d2: C).(wf3 g d1 d2)) in (ex2 C TMP_192 TMP_193)))) in (let +H_x0 \def (H c d1 v H5 g x0 H9 w H3) in (let H11 \def H_x0 in (let TMP_197 +\def (\lambda (d2: C).(let TMP_195 \def (Bind b) in (let TMP_196 \def (CHead +d2 TMP_195 v) in (getl n x0 TMP_196)))) in (let TMP_198 \def (\lambda (d2: +C).(wf3 g d1 d2)) in (let TMP_205 \def (\lambda (d2: C).(let TMP_199 \def (S +n) in (let TMP_200 \def (Bind Void) in (let TMP_201 \def (TSort O) in (let +TMP_202 \def (CHead x0 TMP_200 TMP_201) in (let TMP_203 \def (Bind b) in (let +TMP_204 \def (CHead d2 TMP_203 v) in (getl TMP_199 TMP_202 TMP_204)))))))) in +(let TMP_206 \def (\lambda (d2: C).(wf3 g d1 d2)) in (let TMP_207 \def (ex2 C +TMP_205 TMP_206) in (let TMP_221 \def (\lambda (x: C).(\lambda (H12: (getl n +x0 (CHead x (Bind b) v))).(\lambda (H13: (wf3 g d1 x)).(let TMP_214 \def +(\lambda (d2: C).(let TMP_208 \def (S n) in (let TMP_209 \def (Bind Void) in +(let TMP_210 \def (TSort O) in (let TMP_211 \def (CHead x0 TMP_209 TMP_210) +in (let TMP_212 \def (Bind b) in (let TMP_213 \def (CHead d2 TMP_212 v) in +(getl TMP_208 TMP_211 TMP_213)))))))) in (let TMP_215 \def (\lambda (d2: +C).(wf3 g d1 d2)) in (let TMP_216 \def (Bind Void) in (let TMP_217 \def (Bind +b) in (let TMP_218 \def (CHead x TMP_217 v) in (let TMP_219 \def (TSort O) in +(let TMP_220 \def (getl_head TMP_216 n x0 TMP_218 H12 TMP_219) in (ex_intro2 +C TMP_214 TMP_215 x TMP_220 H13))))))))))) in (let TMP_222 \def (ex2_ind C +TMP_197 TMP_198 TMP_207 TMP_221 H11) in (eq_ind_r C TMP_188 TMP_194 TMP_222 +c2 H8)))))))))))))))))) in (ex3_ind C TMP_177 TMP_178 TMP_179 TMP_185 TMP_223 +H7))))))))) in (or_ind TMP_114 TMP_121 TMP_127 TMP_173 TMP_224 +H6))))))))))))))))))) in (let TMP_226 \def (\lambda (f: F).(\lambda (H4: (wf3 +g (CHead c (Flat f) t) c2)).(\lambda (H5: (getl (r (Flat f) n) c (CHead d1 +(Bind b) v))).(let H_y \def (wf3_gen_flat1 g c c2 t f H4) in (H0 d1 v H5 g c2 +H_y w H3))))) in (let TMP_227 \def (Bind b) in (let TMP_228 \def (CHead d1 +TMP_227 v) in (let TMP_229 \def (getl_gen_S k c TMP_228 t n H1) in (K_ind +TMP_108 TMP_225 TMP_226 k H2 TMP_229))))))))))))))))))) in (C_ind TMP_92 +TMP_102 TMP_230 c1))))))) in (nat_ind TMP_5 TMP_86 TMP_231 i))))). theorem getl_wf3_trans: \forall (i: nat).(\forall (c1: C).(\forall (d1: C).((getl i c1 d1) \to (\forall (g: G).(\forall (d2: C).((wf3 g d1 d2) \to (ex2 C (\lambda (c2: C).(wf3 g c1 c2)) (\lambda (c2: C).(getl i c2 d2))))))))) \def - \lambda (i: nat).(nat_ind (\lambda (n: nat).(\forall (c1: C).(\forall (d1: -C).((getl n c1 d1) \to (\forall (g: G).(\forall (d2: C).((wf3 g d1 d2) \to -(ex2 C (\lambda (c2: C).(wf3 g c1 c2)) (\lambda (c2: C).(getl n c2 -d2)))))))))) (\lambda (c1: C).(\lambda (d1: C).(\lambda (H: (getl O c1 -d1)).(\lambda (g: G).(\lambda (d2: C).(\lambda (H0: (wf3 g d1 d2)).(let H_x -\def (clear_wf3_trans c1 d1 (getl_gen_O c1 d1 H) g d2 H0) in (let H1 \def H_x -in (ex2_ind C (\lambda (c2: C).(wf3 g c1 c2)) (\lambda (c2: C).(clear c2 d2)) -(ex2 C (\lambda (c2: C).(wf3 g c1 c2)) (\lambda (c2: C).(getl O c2 d2))) -(\lambda (x: C).(\lambda (H2: (wf3 g c1 x)).(\lambda (H3: (clear x -d2)).(ex_intro2 C (\lambda (c2: C).(wf3 g c1 c2)) (\lambda (c2: C).(getl O c2 -d2)) x H2 (getl_intro O x d2 x (drop_refl x) H3))))) H1))))))))) (\lambda (n: -nat).(\lambda (H: ((\forall (c1: C).(\forall (d1: C).((getl n c1 d1) \to + \lambda (i: nat).(let TMP_3 \def (\lambda (n: nat).(\forall (c1: C).(\forall +(d1: C).((getl n c1 d1) \to (\forall (g: G).(\forall (d2: C).((wf3 g d1 d2) +\to (let TMP_1 \def (\lambda (c2: C).(wf3 g c1 c2)) in (let TMP_2 \def +(\lambda (c2: C).(getl n c2 d2)) in (ex2 C TMP_1 TMP_2)))))))))) in (let +TMP_15 \def (\lambda (c1: C).(\lambda (d1: C).(\lambda (H: (getl O c1 +d1)).(\lambda (g: G).(\lambda (d2: C).(\lambda (H0: (wf3 g d1 d2)).(let TMP_4 +\def (getl_gen_O c1 d1 H) in (let H_x \def (clear_wf3_trans c1 d1 TMP_4 g d2 +H0) in (let H1 \def H_x in (let TMP_5 \def (\lambda (c2: C).(wf3 g c1 c2)) in +(let TMP_6 \def (\lambda (c2: C).(clear c2 d2)) in (let TMP_7 \def (\lambda +(c2: C).(wf3 g c1 c2)) in (let TMP_8 \def (\lambda (c2: C).(getl O c2 d2)) in +(let TMP_9 \def (ex2 C TMP_7 TMP_8) in (let TMP_14 \def (\lambda (x: +C).(\lambda (H2: (wf3 g c1 x)).(\lambda (H3: (clear x d2)).(let TMP_10 \def +(\lambda (c2: C).(wf3 g c1 c2)) in (let TMP_11 \def (\lambda (c2: C).(getl O +c2 d2)) in (let TMP_12 \def (drop_refl x) in (let TMP_13 \def (getl_intro O x +d2 x TMP_12 H3) in (ex_intro2 C TMP_10 TMP_11 x H2 TMP_13)))))))) in (ex2_ind +C TMP_5 TMP_6 TMP_9 TMP_14 H1)))))))))))))))) in (let TMP_102 \def (\lambda +(n: nat).(\lambda (H: ((\forall (c1: C).(\forall (d1: C).((getl n c1 d1) \to (\forall (g: G).(\forall (d2: C).((wf3 g d1 d2) \to (ex2 C (\lambda (c2: C).(wf3 g c1 c2)) (\lambda (c2: C).(getl n c2 d2))))))))))).(\lambda (c1: -C).(C_ind (\lambda (c: C).(\forall (d1: C).((getl (S n) c d1) \to (\forall -(g: G).(\forall (d2: C).((wf3 g d1 d2) \to (ex2 C (\lambda (c2: C).(wf3 g c -c2)) (\lambda (c2: C).(getl (S n) c2 d2))))))))) (\lambda (n0: nat).(\lambda -(d1: C).(\lambda (H0: (getl (S n) (CSort n0) d1)).(\lambda (g: G).(\lambda -(d2: C).(\lambda (_: (wf3 g d1 d2)).(getl_gen_sort n0 (S n) d1 H0 (ex2 C -(\lambda (c2: C).(wf3 g (CSort n0) c2)) (\lambda (c2: C).(getl (S n) c2 -d2)))))))))) (\lambda (c: C).(\lambda (H0: ((\forall (d1: C).((getl (S n) c +C).(let TMP_19 \def (\lambda (c: C).(\forall (d1: C).((getl (S n) c d1) \to +(\forall (g: G).(\forall (d2: C).((wf3 g d1 d2) \to (let TMP_16 \def (\lambda +(c2: C).(wf3 g c c2)) in (let TMP_18 \def (\lambda (c2: C).(let TMP_17 \def +(S n) in (getl TMP_17 c2 d2))) in (ex2 C TMP_16 TMP_18))))))))) in (let +TMP_26 \def (\lambda (n0: nat).(\lambda (d1: C).(\lambda (H0: (getl (S n) +(CSort n0) d1)).(\lambda (g: G).(\lambda (d2: C).(\lambda (_: (wf3 g d1 +d2)).(let TMP_20 \def (S n) in (let TMP_22 \def (\lambda (c2: C).(let TMP_21 +\def (CSort n0) in (wf3 g TMP_21 c2))) in (let TMP_24 \def (\lambda (c2: +C).(let TMP_23 \def (S n) in (getl TMP_23 c2 d2))) in (let TMP_25 \def (ex2 C +TMP_22 TMP_24) in (getl_gen_sort n0 TMP_20 d1 H0 TMP_25))))))))))) in (let +TMP_101 \def (\lambda (c: C).(\lambda (H0: ((\forall (d1: C).((getl (S n) c d1) \to (\forall (g: G).(\forall (d2: C).((wf3 g d1 d2) \to (ex2 C (\lambda (c2: C).(wf3 g c c2)) (\lambda (c2: C).(getl (S n) c2 d2)))))))))).(\lambda (k: K).(\lambda (t: T).(\lambda (d1: C).(\lambda (H1: (getl (S n) (CHead c k -t) d1)).(\lambda (g: G).(\lambda (d2: C).(\lambda (H2: (wf3 g d1 d2)).(K_ind -(\lambda (k0: K).((getl (r k0 n) c d1) \to (ex2 C (\lambda (c2: C).(wf3 g -(CHead c k0 t) c2)) (\lambda (c2: C).(getl (S n) c2 d2))))) (\lambda (b: +t) d1)).(\lambda (g: G).(\lambda (d2: C).(\lambda (H2: (wf3 g d1 d2)).(let +TMP_31 \def (\lambda (k0: K).((getl (r k0 n) c d1) \to (let TMP_28 \def +(\lambda (c2: C).(let TMP_27 \def (CHead c k0 t) in (wf3 g TMP_27 c2))) in +(let TMP_30 \def (\lambda (c2: C).(let TMP_29 \def (S n) in (getl TMP_29 c2 +d2))) in (ex2 C TMP_28 TMP_30))))) in (let TMP_82 \def (\lambda (b: B).(\lambda (H3: (getl (r (Bind b) n) c d1)).(let H_x \def (H c d1 H3 g d2 -H2) in (let H4 \def H_x in (ex2_ind C (\lambda (c2: C).(wf3 g c c2)) (\lambda -(c2: C).(getl n c2 d2)) (ex2 C (\lambda (c2: C).(wf3 g (CHead c (Bind b) t) -c2)) (\lambda (c2: C).(getl (S n) c2 d2))) (\lambda (x: C).(\lambda (H5: (wf3 -g c x)).(\lambda (H6: (getl n x d2)).(let H_x0 \def (ty3_inference g c t) in -(let H7 \def H_x0 in (or_ind (ex T (\lambda (t2: T).(ty3 g c t t2))) (\forall -(t2: T).((ty3 g c t t2) \to False)) (ex2 C (\lambda (c2: C).(wf3 g (CHead c -(Bind b) t) c2)) (\lambda (c2: C).(getl (S n) c2 d2))) (\lambda (H8: (ex T -(\lambda (t2: T).(ty3 g c t t2)))).(ex_ind T (\lambda (t2: T).(ty3 g c t t2)) -(ex2 C (\lambda (c2: C).(wf3 g (CHead c (Bind b) t) c2)) (\lambda (c2: -C).(getl (S n) c2 d2))) (\lambda (x0: T).(\lambda (H9: (ty3 g c t -x0)).(ex_intro2 C (\lambda (c2: C).(wf3 g (CHead c (Bind b) t) c2)) (\lambda -(c2: C).(getl (S n) c2 d2)) (CHead x (Bind b) t) (wf3_bind g c x H5 t x0 H9 -b) (getl_head (Bind b) n x d2 H6 t)))) H8)) (\lambda (H8: ((\forall (t2: -T).((ty3 g c t t2) \to False)))).(ex_intro2 C (\lambda (c2: C).(wf3 g (CHead -c (Bind b) t) c2)) (\lambda (c2: C).(getl (S n) c2 d2)) (CHead x (Bind Void) -(TSort O)) (wf3_void g c x H5 t H8 b) (getl_head (Bind Void) n x d2 H6 (TSort -O)))) H7)))))) H4))))) (\lambda (f: F).(\lambda (H3: (getl (r (Flat f) n) c -d1)).(let H_x \def (H0 d1 H3 g d2 H2) in (let H4 \def H_x in (ex2_ind C -(\lambda (c2: C).(wf3 g c c2)) (\lambda (c2: C).(getl (S n) c2 d2)) (ex2 C -(\lambda (c2: C).(wf3 g (CHead c (Flat f) t) c2)) (\lambda (c2: C).(getl (S -n) c2 d2))) (\lambda (x: C).(\lambda (H5: (wf3 g c x)).(\lambda (H6: (getl (S -n) x d2)).(ex_intro2 C (\lambda (c2: C).(wf3 g (CHead c (Flat f) t) c2)) -(\lambda (c2: C).(getl (S n) c2 d2)) x (wf3_flat g c x H5 t f) H6)))) H4))))) -k (getl_gen_S k c d1 t n H1))))))))))) c1)))) i). -(* COMMENTS -Initial nodes: 1139 -END *) +H2) in (let H4 \def H_x in (let TMP_32 \def (\lambda (c2: C).(wf3 g c c2)) in +(let TMP_33 \def (\lambda (c2: C).(getl n c2 d2)) in (let TMP_36 \def +(\lambda (c2: C).(let TMP_34 \def (Bind b) in (let TMP_35 \def (CHead c +TMP_34 t) in (wf3 g TMP_35 c2)))) in (let TMP_38 \def (\lambda (c2: C).(let +TMP_37 \def (S n) in (getl TMP_37 c2 d2))) in (let TMP_39 \def (ex2 C TMP_36 +TMP_38) in (let TMP_81 \def (\lambda (x: C).(\lambda (H5: (wf3 g c +x)).(\lambda (H6: (getl n x d2)).(let H_x0 \def (ty3_inference g c t) in (let +H7 \def H_x0 in (let TMP_40 \def (\lambda (t2: T).(ty3 g c t t2)) in (let +TMP_41 \def (ex T TMP_40) in (let TMP_42 \def (\forall (t2: T).((ty3 g c t +t2) \to False)) in (let TMP_45 \def (\lambda (c2: C).(let TMP_43 \def (Bind +b) in (let TMP_44 \def (CHead c TMP_43 t) in (wf3 g TMP_44 c2)))) in (let +TMP_47 \def (\lambda (c2: C).(let TMP_46 \def (S n) in (getl TMP_46 c2 d2))) +in (let TMP_48 \def (ex2 C TMP_45 TMP_47) in (let TMP_67 \def (\lambda (H8: +(ex T (\lambda (t2: T).(ty3 g c t t2)))).(let TMP_49 \def (\lambda (t2: +T).(ty3 g c t t2)) in (let TMP_52 \def (\lambda (c2: C).(let TMP_50 \def +(Bind b) in (let TMP_51 \def (CHead c TMP_50 t) in (wf3 g TMP_51 c2)))) in +(let TMP_54 \def (\lambda (c2: C).(let TMP_53 \def (S n) in (getl TMP_53 c2 +d2))) in (let TMP_55 \def (ex2 C TMP_52 TMP_54) in (let TMP_66 \def (\lambda +(x0: T).(\lambda (H9: (ty3 g c t x0)).(let TMP_58 \def (\lambda (c2: C).(let +TMP_56 \def (Bind b) in (let TMP_57 \def (CHead c TMP_56 t) in (wf3 g TMP_57 +c2)))) in (let TMP_60 \def (\lambda (c2: C).(let TMP_59 \def (S n) in (getl +TMP_59 c2 d2))) in (let TMP_61 \def (Bind b) in (let TMP_62 \def (CHead x +TMP_61 t) in (let TMP_63 \def (wf3_bind g c x H5 t x0 H9 b) in (let TMP_64 +\def (Bind b) in (let TMP_65 \def (getl_head TMP_64 n x d2 H6 t) in +(ex_intro2 C TMP_58 TMP_60 TMP_62 TMP_63 TMP_65)))))))))) in (ex_ind T TMP_49 +TMP_55 TMP_66 H8))))))) in (let TMP_80 \def (\lambda (H8: ((\forall (t2: +T).((ty3 g c t t2) \to False)))).(let TMP_70 \def (\lambda (c2: C).(let +TMP_68 \def (Bind b) in (let TMP_69 \def (CHead c TMP_68 t) in (wf3 g TMP_69 +c2)))) in (let TMP_72 \def (\lambda (c2: C).(let TMP_71 \def (S n) in (getl +TMP_71 c2 d2))) in (let TMP_73 \def (Bind Void) in (let TMP_74 \def (TSort O) +in (let TMP_75 \def (CHead x TMP_73 TMP_74) in (let TMP_76 \def (wf3_void g c +x H5 t H8 b) in (let TMP_77 \def (Bind Void) in (let TMP_78 \def (TSort O) in +(let TMP_79 \def (getl_head TMP_77 n x d2 H6 TMP_78) in (ex_intro2 C TMP_70 +TMP_72 TMP_75 TMP_76 TMP_79))))))))))) in (or_ind TMP_41 TMP_42 TMP_48 TMP_67 +TMP_80 H7)))))))))))))) in (ex2_ind C TMP_32 TMP_33 TMP_39 TMP_81 +H4))))))))))) in (let TMP_99 \def (\lambda (f: F).(\lambda (H3: (getl (r +(Flat f) n) c d1)).(let H_x \def (H0 d1 H3 g d2 H2) in (let H4 \def H_x in +(let TMP_83 \def (\lambda (c2: C).(wf3 g c c2)) in (let TMP_85 \def (\lambda +(c2: C).(let TMP_84 \def (S n) in (getl TMP_84 c2 d2))) in (let TMP_88 \def +(\lambda (c2: C).(let TMP_86 \def (Flat f) in (let TMP_87 \def (CHead c +TMP_86 t) in (wf3 g TMP_87 c2)))) in (let TMP_90 \def (\lambda (c2: C).(let +TMP_89 \def (S n) in (getl TMP_89 c2 d2))) in (let TMP_91 \def (ex2 C TMP_88 +TMP_90) in (let TMP_98 \def (\lambda (x: C).(\lambda (H5: (wf3 g c +x)).(\lambda (H6: (getl (S n) x d2)).(let TMP_94 \def (\lambda (c2: C).(let +TMP_92 \def (Flat f) in (let TMP_93 \def (CHead c TMP_92 t) in (wf3 g TMP_93 +c2)))) in (let TMP_96 \def (\lambda (c2: C).(let TMP_95 \def (S n) in (getl +TMP_95 c2 d2))) in (let TMP_97 \def (wf3_flat g c x H5 t f) in (ex_intro2 C +TMP_94 TMP_96 x TMP_97 H6))))))) in (ex2_ind C TMP_83 TMP_85 TMP_91 TMP_98 +H4))))))))))) in (let TMP_100 \def (getl_gen_S k c d1 t n H1) in (K_ind +TMP_31 TMP_82 TMP_99 k TMP_100)))))))))))))) in (C_ind TMP_19 TMP_26 TMP_101 +c1))))))) in (nat_ind TMP_3 TMP_15 TMP_102 i)))). diff --git a/matita/matita/contribs/lambdadelta/basic_1/wf3/props.ma b/matita/matita/contribs/lambdadelta/basic_1/wf3/props.ma index 98a05c637..4aabeb81e 100644 --- a/matita/matita/contribs/lambdadelta/basic_1/wf3/props.ma +++ b/matita/matita/contribs/lambdadelta/basic_1/wf3/props.ma @@ -14,222 +14,221 @@ (* This file was automatically generated: do not edit *********************) -include "Basic-1/wf3/ty3.ma". +include "basic_1/wf3/ty3.ma". -include "Basic-1/app/defs.ma". - -theorem wf3_mono: - \forall (g: G).(\forall (c: C).(\forall (c1: C).((wf3 g c c1) \to (\forall -(c2: C).((wf3 g c c2) \to (eq C c1 c2)))))) -\def - \lambda (g: G).(\lambda (c: C).(\lambda (c1: C).(\lambda (H: (wf3 g c -c1)).(wf3_ind g (\lambda (c0: C).(\lambda (c2: C).(\forall (c3: C).((wf3 g c0 -c3) \to (eq C c2 c3))))) (\lambda (m: nat).(\lambda (c2: C).(\lambda (H0: -(wf3 g (CSort m) c2)).(let H_y \def (wf3_gen_sort1 g c2 m H0) in (eq_ind_r C -(CSort m) (\lambda (c0: C).(eq C (CSort m) c0)) (refl_equal C (CSort m)) c2 -H_y))))) (\lambda (c2: C).(\lambda (c3: C).(\lambda (_: (wf3 g c2 -c3)).(\lambda (H1: ((\forall (c4: C).((wf3 g c2 c4) \to (eq C c3 -c4))))).(\lambda (u: T).(\lambda (t: T).(\lambda (H2: (ty3 g c2 u -t)).(\lambda (b: B).(\lambda (c0: C).(\lambda (H3: (wf3 g (CHead c2 (Bind b) -u) c0)).(let H_x \def (wf3_gen_bind1 g c2 c0 u b H3) in (let H4 \def H_x in -(or_ind (ex3_2 C T (\lambda (c4: C).(\lambda (_: T).(eq C c0 (CHead c4 (Bind -b) u)))) (\lambda (c4: C).(\lambda (_: T).(wf3 g c2 c4))) (\lambda (_: -C).(\lambda (w: T).(ty3 g c2 u w)))) (ex3 C (\lambda (c4: C).(eq C c0 (CHead -c4 (Bind Void) (TSort O)))) (\lambda (c4: C).(wf3 g c2 c4)) (\lambda (_: -C).(\forall (w: T).((ty3 g c2 u w) \to False)))) (eq C (CHead c3 (Bind b) u) -c0) (\lambda (H5: (ex3_2 C T (\lambda (c4: C).(\lambda (_: T).(eq C c0 (CHead -c4 (Bind b) u)))) (\lambda (c4: C).(\lambda (_: T).(wf3 g c2 c4))) (\lambda -(_: C).(\lambda (w: T).(ty3 g c2 u w))))).(ex3_2_ind C T (\lambda (c4: -C).(\lambda (_: T).(eq C c0 (CHead c4 (Bind b) u)))) (\lambda (c4: -C).(\lambda (_: T).(wf3 g c2 c4))) (\lambda (_: C).(\lambda (w: T).(ty3 g c2 -u w))) (eq C (CHead c3 (Bind b) u) c0) (\lambda (x0: C).(\lambda (x1: -T).(\lambda (H6: (eq C c0 (CHead x0 (Bind b) u))).(\lambda (H7: (wf3 g c2 -x0)).(\lambda (_: (ty3 g c2 u x1)).(eq_ind_r C (CHead x0 (Bind b) u) (\lambda -(c4: C).(eq C (CHead c3 (Bind b) u) c4)) (f_equal3 C K T C CHead c3 x0 (Bind -b) (Bind b) u u (H1 x0 H7) (refl_equal K (Bind b)) (refl_equal T u)) c0 -H6)))))) H5)) (\lambda (H5: (ex3 C (\lambda (c4: C).(eq C c0 (CHead c4 (Bind -Void) (TSort O)))) (\lambda (c4: C).(wf3 g c2 c4)) (\lambda (_: C).(\forall -(w: T).((ty3 g c2 u w) \to False))))).(ex3_ind C (\lambda (c4: C).(eq C c0 -(CHead c4 (Bind Void) (TSort O)))) (\lambda (c4: C).(wf3 g c2 c4)) (\lambda -(_: C).(\forall (w: T).((ty3 g c2 u w) \to False))) (eq C (CHead c3 (Bind b) -u) c0) (\lambda (x0: C).(\lambda (H6: (eq C c0 (CHead x0 (Bind Void) (TSort -O)))).(\lambda (_: (wf3 g c2 x0)).(\lambda (H8: ((\forall (w: T).((ty3 g c2 u -w) \to False)))).(eq_ind_r C (CHead x0 (Bind Void) (TSort O)) (\lambda (c4: -C).(eq C (CHead c3 (Bind b) u) c4)) (let H_x0 \def (H8 t H2) in (let H9 \def -H_x0 in (False_ind (eq C (CHead c3 (Bind b) u) (CHead x0 (Bind Void) (TSort -O))) H9))) c0 H6))))) H5)) H4))))))))))))) (\lambda (c2: C).(\lambda (c3: -C).(\lambda (_: (wf3 g c2 c3)).(\lambda (H1: ((\forall (c4: C).((wf3 g c2 c4) -\to (eq C c3 c4))))).(\lambda (u: T).(\lambda (H2: ((\forall (t: T).((ty3 g -c2 u t) \to False)))).(\lambda (b: B).(\lambda (c0: C).(\lambda (H3: (wf3 g -(CHead c2 (Bind b) u) c0)).(let H_x \def (wf3_gen_bind1 g c2 c0 u b H3) in -(let H4 \def H_x in (or_ind (ex3_2 C T (\lambda (c4: C).(\lambda (_: T).(eq C -c0 (CHead c4 (Bind b) u)))) (\lambda (c4: C).(\lambda (_: T).(wf3 g c2 c4))) -(\lambda (_: C).(\lambda (w: T).(ty3 g c2 u w)))) (ex3 C (\lambda (c4: C).(eq -C c0 (CHead c4 (Bind Void) (TSort O)))) (\lambda (c4: C).(wf3 g c2 c4)) -(\lambda (_: C).(\forall (w: T).((ty3 g c2 u w) \to False)))) (eq C (CHead c3 -(Bind Void) (TSort O)) c0) (\lambda (H5: (ex3_2 C T (\lambda (c4: C).(\lambda -(_: T).(eq C c0 (CHead c4 (Bind b) u)))) (\lambda (c4: C).(\lambda (_: -T).(wf3 g c2 c4))) (\lambda (_: C).(\lambda (w: T).(ty3 g c2 u -w))))).(ex3_2_ind C T (\lambda (c4: C).(\lambda (_: T).(eq C c0 (CHead c4 -(Bind b) u)))) (\lambda (c4: C).(\lambda (_: T).(wf3 g c2 c4))) (\lambda (_: -C).(\lambda (w: T).(ty3 g c2 u w))) (eq C (CHead c3 (Bind Void) (TSort O)) -c0) (\lambda (x0: C).(\lambda (x1: T).(\lambda (H6: (eq C c0 (CHead x0 (Bind -b) u))).(\lambda (_: (wf3 g c2 x0)).(\lambda (H8: (ty3 g c2 u x1)).(eq_ind_r -C (CHead x0 (Bind b) u) (\lambda (c4: C).(eq C (CHead c3 (Bind Void) (TSort -O)) c4)) (let H_x0 \def (H2 x1 H8) in (let H9 \def H_x0 in (False_ind (eq C -(CHead c3 (Bind Void) (TSort O)) (CHead x0 (Bind b) u)) H9))) c0 H6)))))) -H5)) (\lambda (H5: (ex3 C (\lambda (c4: C).(eq C c0 (CHead c4 (Bind Void) -(TSort O)))) (\lambda (c4: C).(wf3 g c2 c4)) (\lambda (_: C).(\forall (w: -T).((ty3 g c2 u w) \to False))))).(ex3_ind C (\lambda (c4: C).(eq C c0 (CHead -c4 (Bind Void) (TSort O)))) (\lambda (c4: C).(wf3 g c2 c4)) (\lambda (_: -C).(\forall (w: T).((ty3 g c2 u w) \to False))) (eq C (CHead c3 (Bind Void) -(TSort O)) c0) (\lambda (x0: C).(\lambda (H6: (eq C c0 (CHead x0 (Bind Void) -(TSort O)))).(\lambda (H7: (wf3 g c2 x0)).(\lambda (_: ((\forall (w: T).((ty3 -g c2 u w) \to False)))).(eq_ind_r C (CHead x0 (Bind Void) (TSort O)) (\lambda -(c4: C).(eq C (CHead c3 (Bind Void) (TSort O)) c4)) (f_equal3 C K T C CHead -c3 x0 (Bind Void) (Bind Void) (TSort O) (TSort O) (H1 x0 H7) (refl_equal K -(Bind Void)) (refl_equal T (TSort O))) c0 H6))))) H5)) H4)))))))))))) -(\lambda (c2: C).(\lambda (c3: C).(\lambda (_: (wf3 g c2 c3)).(\lambda (H1: -((\forall (c4: C).((wf3 g c2 c4) \to (eq C c3 c4))))).(\lambda (u: -T).(\lambda (f: F).(\lambda (c0: C).(\lambda (H2: (wf3 g (CHead c2 (Flat f) -u) c0)).(let H_y \def (wf3_gen_flat1 g c2 c0 u f H2) in (H1 c0 H_y)))))))))) -c c1 H)))). -(* COMMENTS -Initial nodes: 1555 -END *) +include "basic_1/app/defs.ma". theorem wf3_total: \forall (g: G).(\forall (c1: C).(ex C (\lambda (c2: C).(wf3 g c1 c2)))) \def - \lambda (g: G).(\lambda (c1: C).(C_ind (\lambda (c: C).(ex C (\lambda (c2: -C).(wf3 g c c2)))) (\lambda (n: nat).(ex_intro C (\lambda (c2: C).(wf3 g -(CSort n) c2)) (CSort n) (wf3_sort g n))) (\lambda (c: C).(\lambda (H: (ex C -(\lambda (c2: C).(wf3 g c c2)))).(\lambda (k: K).(\lambda (t: T).(let H0 \def -H in (ex_ind C (\lambda (c2: C).(wf3 g c c2)) (ex C (\lambda (c2: C).(wf3 g -(CHead c k t) c2))) (\lambda (x: C).(\lambda (H1: (wf3 g c x)).(K_ind -(\lambda (k0: K).(ex C (\lambda (c2: C).(wf3 g (CHead c k0 t) c2)))) (\lambda -(b: B).(let H_x \def (ty3_inference g c t) in (let H2 \def H_x in (or_ind (ex -T (\lambda (t2: T).(ty3 g c t t2))) (\forall (t2: T).((ty3 g c t t2) \to -False)) (ex C (\lambda (c2: C).(wf3 g (CHead c (Bind b) t) c2))) (\lambda -(H3: (ex T (\lambda (t2: T).(ty3 g c t t2)))).(ex_ind T (\lambda (t2: T).(ty3 -g c t t2)) (ex C (\lambda (c2: C).(wf3 g (CHead c (Bind b) t) c2))) (\lambda -(x0: T).(\lambda (H4: (ty3 g c t x0)).(ex_intro C (\lambda (c2: C).(wf3 g -(CHead c (Bind b) t) c2)) (CHead x (Bind b) t) (wf3_bind g c x H1 t x0 H4 -b)))) H3)) (\lambda (H3: ((\forall (t2: T).((ty3 g c t t2) \to -False)))).(ex_intro C (\lambda (c2: C).(wf3 g (CHead c (Bind b) t) c2)) -(CHead x (Bind Void) (TSort O)) (wf3_void g c x H1 t H3 b))) H2)))) (\lambda -(f: F).(ex_intro C (\lambda (c2: C).(wf3 g (CHead c (Flat f) t) c2)) x -(wf3_flat g c x H1 t f))) k))) H0)))))) c1)). -(* COMMENTS -Initial nodes: 435 -END *) + \lambda (g: G).(\lambda (c1: C).(let TMP_2 \def (\lambda (c: C).(let TMP_1 +\def (\lambda (c2: C).(wf3 g c c2)) in (ex C TMP_1))) in (let TMP_7 \def +(\lambda (n: nat).(let TMP_4 \def (\lambda (c2: C).(let TMP_3 \def (CSort n) +in (wf3 g TMP_3 c2))) in (let TMP_5 \def (CSort n) in (let TMP_6 \def +(wf3_sort g n) in (ex_intro C TMP_4 TMP_5 TMP_6))))) in (let TMP_50 \def +(\lambda (c: C).(\lambda (H: (ex C (\lambda (c2: C).(wf3 g c c2)))).(\lambda +(k: K).(\lambda (t: T).(let H0 \def H in (let TMP_8 \def (\lambda (c2: +C).(wf3 g c c2)) in (let TMP_10 \def (\lambda (c2: C).(let TMP_9 \def (CHead +c k t) in (wf3 g TMP_9 c2))) in (let TMP_11 \def (ex C TMP_10) in (let TMP_49 +\def (\lambda (x: C).(\lambda (H1: (wf3 g c x)).(let TMP_14 \def (\lambda +(k0: K).(let TMP_13 \def (\lambda (c2: C).(let TMP_12 \def (CHead c k0 t) in +(wf3 g TMP_12 c2))) in (ex C TMP_13))) in (let TMP_43 \def (\lambda (b: +B).(let H_x \def (ty3_inference g c t) in (let H2 \def H_x in (let TMP_15 +\def (\lambda (t2: T).(ty3 g c t t2)) in (let TMP_16 \def (ex T TMP_15) in +(let TMP_17 \def (\forall (t2: T).((ty3 g c t t2) \to False)) in (let TMP_20 +\def (\lambda (c2: C).(let TMP_18 \def (Bind b) in (let TMP_19 \def (CHead c +TMP_18 t) in (wf3 g TMP_19 c2)))) in (let TMP_21 \def (ex C TMP_20) in (let +TMP_34 \def (\lambda (H3: (ex T (\lambda (t2: T).(ty3 g c t t2)))).(let +TMP_22 \def (\lambda (t2: T).(ty3 g c t t2)) in (let TMP_25 \def (\lambda +(c2: C).(let TMP_23 \def (Bind b) in (let TMP_24 \def (CHead c TMP_23 t) in +(wf3 g TMP_24 c2)))) in (let TMP_26 \def (ex C TMP_25) in (let TMP_33 \def +(\lambda (x0: T).(\lambda (H4: (ty3 g c t x0)).(let TMP_29 \def (\lambda (c2: +C).(let TMP_27 \def (Bind b) in (let TMP_28 \def (CHead c TMP_27 t) in (wf3 g +TMP_28 c2)))) in (let TMP_30 \def (Bind b) in (let TMP_31 \def (CHead x +TMP_30 t) in (let TMP_32 \def (wf3_bind g c x H1 t x0 H4 b) in (ex_intro C +TMP_29 TMP_31 TMP_32))))))) in (ex_ind T TMP_22 TMP_26 TMP_33 H3)))))) in +(let TMP_42 \def (\lambda (H3: ((\forall (t2: T).((ty3 g c t t2) \to +False)))).(let TMP_37 \def (\lambda (c2: C).(let TMP_35 \def (Bind b) in (let +TMP_36 \def (CHead c TMP_35 t) in (wf3 g TMP_36 c2)))) in (let TMP_38 \def +(Bind Void) in (let TMP_39 \def (TSort O) in (let TMP_40 \def (CHead x TMP_38 +TMP_39) in (let TMP_41 \def (wf3_void g c x H1 t H3 b) in (ex_intro C TMP_37 +TMP_40 TMP_41))))))) in (or_ind TMP_16 TMP_17 TMP_21 TMP_34 TMP_42 +H2))))))))))) in (let TMP_48 \def (\lambda (f: F).(let TMP_46 \def (\lambda +(c2: C).(let TMP_44 \def (Flat f) in (let TMP_45 \def (CHead c TMP_44 t) in +(wf3 g TMP_45 c2)))) in (let TMP_47 \def (wf3_flat g c x H1 t f) in (ex_intro +C TMP_46 x TMP_47)))) in (K_ind TMP_14 TMP_43 TMP_48 k)))))) in (ex_ind C +TMP_8 TMP_11 TMP_49 H0)))))))))) in (C_ind TMP_2 TMP_7 TMP_50 c1))))). theorem ty3_shift1: \forall (g: G).(\forall (c: C).((wf3 g c c) \to (\forall (t1: T).(\forall (t2: T).((ty3 g c t1 t2) \to (ty3 g (CSort (cbk c)) (app1 c t1) (app1 c t2))))))) \def - \lambda (g: G).(\lambda (c: C).(\lambda (H: (wf3 g c c)).(insert_eq C c -(\lambda (c0: C).(wf3 g c0 c)) (\lambda (c0: C).(\forall (t1: T).(\forall -(t2: T).((ty3 g c0 t1 t2) \to (ty3 g (CSort (cbk c0)) (app1 c0 t1) (app1 c0 -t2)))))) (\lambda (y: C).(\lambda (H0: (wf3 g y c)).(wf3_ind g (\lambda (c0: + \lambda (g: G).(\lambda (c: C).(\lambda (H: (wf3 g c c)).(let TMP_1 \def +(\lambda (c0: C).(wf3 g c0 c)) in (let TMP_6 \def (\lambda (c0: C).(\forall +(t1: T).(\forall (t2: T).((ty3 g c0 t1 t2) \to (let TMP_2 \def (cbk c0) in +(let TMP_3 \def (CSort TMP_2) in (let TMP_4 \def (app1 c0 t1) in (let TMP_5 +\def (app1 c0 t2) in (ty3 g TMP_3 TMP_4 TMP_5))))))))) in (let TMP_180 \def +(\lambda (y: C).(\lambda (H0: (wf3 g y c)).(let TMP_11 \def (\lambda (c0: C).(\lambda (c1: C).((eq C c0 c1) \to (\forall (t1: T).(\forall (t2: T).((ty3 -g c0 t1 t2) \to (ty3 g (CSort (cbk c0)) (app1 c0 t1) (app1 c0 t2)))))))) -(\lambda (m: nat).(\lambda (_: (eq C (CSort m) (CSort m))).(\lambda (t1: -T).(\lambda (t2: T).(\lambda (H2: (ty3 g (CSort m) t1 t2)).H2))))) (\lambda -(c1: C).(\lambda (c2: C).(\lambda (H1: (wf3 g c1 c2)).(\lambda (H2: (((eq C -c1 c2) \to (\forall (t1: T).(\forall (t2: T).((ty3 g c1 t1 t2) \to (ty3 g -(CSort (cbk c1)) (app1 c1 t1) (app1 c1 t2)))))))).(\lambda (u: T).(\lambda -(t: T).(\lambda (H3: (ty3 g c1 u t)).(\lambda (b: B).(\lambda (H4: (eq C -(CHead c1 (Bind b) u) (CHead c2 (Bind b) u))).(\lambda (t1: T).(\lambda (t2: -T).(\lambda (H5: (ty3 g (CHead c1 (Bind b) u) t1 t2)).(let H6 \def (f_equal C -C (\lambda (e: C).(match e in C return (\lambda (_: C).C) with [(CSort _) -\Rightarrow c1 | (CHead c0 _ _) \Rightarrow c0])) (CHead c1 (Bind b) u) -(CHead c2 (Bind b) u) H4) in (let H7 \def (eq_ind_r C c2 (\lambda (c0: -C).((eq C c1 c0) \to (\forall (t3: T).(\forall (t4: T).((ty3 g c1 t3 t4) \to -(ty3 g (CSort (cbk c1)) (app1 c1 t3) (app1 c1 t4))))))) H2 c1 H6) in (let H8 -\def (eq_ind_r C c2 (\lambda (c0: C).(wf3 g c1 c0)) H1 c1 H6) in (ex_ind T -(\lambda (t0: T).(ty3 g (CHead c1 (Bind b) u) t2 t0)) (ty3 g (CSort (cbk c1)) -(app1 c1 (THead (Bind b) u t1)) (app1 c1 (THead (Bind b) u t2))) (\lambda (x: -T).(\lambda (_: (ty3 g (CHead c1 (Bind b) u) t2 x)).(H7 (refl_equal C c1) -(THead (Bind b) u t1) (THead (Bind b) u t2) (ty3_bind g c1 u t H3 b t1 t2 -H5)))) (ty3_correct g (CHead c1 (Bind b) u) t1 t2 H5))))))))))))))))) -(\lambda (c1: C).(\lambda (c2: C).(\lambda (H1: (wf3 g c1 c2)).(\lambda (H2: -(((eq C c1 c2) \to (\forall (t1: T).(\forall (t2: T).((ty3 g c1 t1 t2) \to -(ty3 g (CSort (cbk c1)) (app1 c1 t1) (app1 c1 t2)))))))).(\lambda (u: -T).(\lambda (H3: ((\forall (t: T).((ty3 g c1 u t) \to False)))).(\lambda (b: -B).(\lambda (H4: (eq C (CHead c1 (Bind b) u) (CHead c2 (Bind Void) (TSort -O)))).(\lambda (t1: T).(\lambda (t2: T).(\lambda (H5: (ty3 g (CHead c1 (Bind -b) u) t1 t2)).(let H6 \def (f_equal C C (\lambda (e: C).(match e in C return -(\lambda (_: C).C) with [(CSort _) \Rightarrow c1 | (CHead c0 _ _) -\Rightarrow c0])) (CHead c1 (Bind b) u) (CHead c2 (Bind Void) (TSort O)) H4) -in ((let H7 \def (f_equal C B (\lambda (e: C).(match e in C return (\lambda -(_: C).B) with [(CSort _) \Rightarrow b | (CHead _ k _) \Rightarrow (match k -in K return (\lambda (_: K).B) with [(Bind b0) \Rightarrow b0 | (Flat _) -\Rightarrow b])])) (CHead c1 (Bind b) u) (CHead c2 (Bind Void) (TSort O)) H4) -in ((let H8 \def (f_equal C T (\lambda (e: C).(match e in C return (\lambda -(_: C).T) with [(CSort _) \Rightarrow u | (CHead _ _ t) \Rightarrow t])) -(CHead c1 (Bind b) u) (CHead c2 (Bind Void) (TSort O)) H4) in (\lambda (H9: -(eq B b Void)).(\lambda (H10: (eq C c1 c2)).(let H11 \def (eq_ind B b -(\lambda (b0: B).(ty3 g (CHead c1 (Bind b0) u) t1 t2)) H5 Void H9) in -(eq_ind_r B Void (\lambda (b0: B).(ty3 g (CSort (cbk (CHead c1 (Bind b0) u))) -(app1 (CHead c1 (Bind b0) u) t1) (app1 (CHead c1 (Bind b0) u) t2))) (let H12 -\def (eq_ind T u (\lambda (t: T).(ty3 g (CHead c1 (Bind Void) t) t1 t2)) H11 -(TSort O) H8) in (let H13 \def (eq_ind T u (\lambda (t: T).(\forall (t0: -T).((ty3 g c1 t t0) \to False))) H3 (TSort O) H8) in (eq_ind_r T (TSort O) -(\lambda (t: T).(ty3 g (CSort (cbk (CHead c1 (Bind Void) t))) (app1 (CHead c1 -(Bind Void) t) t1) (app1 (CHead c1 (Bind Void) t) t2))) (let H14 \def -(eq_ind_r C c2 (\lambda (c0: C).((eq C c1 c0) \to (\forall (t3: T).(\forall -(t4: T).((ty3 g c1 t3 t4) \to (ty3 g (CSort (cbk c1)) (app1 c1 t3) (app1 c1 -t4))))))) H2 c1 H10) in (let H15 \def (eq_ind_r C c2 (\lambda (c0: C).(wf3 g -c1 c0)) H1 c1 H10) in (ex_ind T (\lambda (t: T).(ty3 g (CHead c1 (Bind Void) -(TSort O)) t2 t)) (ty3 g (CSort (cbk c1)) (app1 c1 (THead (Bind Void) (TSort -O) t1)) (app1 c1 (THead (Bind Void) (TSort O) t2))) (\lambda (x: T).(\lambda -(_: (ty3 g (CHead c1 (Bind Void) (TSort O)) t2 x)).(H14 (refl_equal C c1) -(THead (Bind Void) (TSort O) t1) (THead (Bind Void) (TSort O) t2) (ty3_bind g -c1 (TSort O) (TSort (next g O)) (ty3_sort g c1 O) Void t1 t2 H12)))) -(ty3_correct g (CHead c1 (Bind Void) (TSort O)) t1 t2 H12)))) u H8))) b -H9))))) H7)) H6))))))))))))) (\lambda (c1: C).(\lambda (c2: C).(\lambda (H1: -(wf3 g c1 c2)).(\lambda (H2: (((eq C c1 c2) \to (\forall (t1: T).(\forall -(t2: T).((ty3 g c1 t1 t2) \to (ty3 g (CSort (cbk c1)) (app1 c1 t1) (app1 c1 +g c0 t1 t2) \to (let TMP_7 \def (cbk c0) in (let TMP_8 \def (CSort TMP_7) in +(let TMP_9 \def (app1 c0 t1) in (let TMP_10 \def (app1 c0 t2) in (ty3 g TMP_8 +TMP_9 TMP_10))))))))))) in (let TMP_12 \def (\lambda (m: nat).(\lambda (_: +(eq C (CSort m) (CSort m))).(\lambda (t1: T).(\lambda (t2: T).(\lambda (H2: +(ty3 g (CSort m) t1 t2)).H2))))) in (let TMP_46 \def (\lambda (c1: +C).(\lambda (c2: C).(\lambda (H1: (wf3 g c1 c2)).(\lambda (H2: (((eq C c1 c2) +\to (\forall (t1: T).(\forall (t2: T).((ty3 g c1 t1 t2) \to (ty3 g (CSort +(cbk c1)) (app1 c1 t1) (app1 c1 t2)))))))).(\lambda (u: T).(\lambda (t: +T).(\lambda (H3: (ty3 g c1 u t)).(\lambda (b: B).(\lambda (H4: (eq C (CHead +c1 (Bind b) u) (CHead c2 (Bind b) u))).(\lambda (t1: T).(\lambda (t2: +T).(\lambda (H5: (ty3 g (CHead c1 (Bind b) u) t1 t2)).(let TMP_13 \def +(\lambda (e: C).(match e with [(CSort _) \Rightarrow c1 | (CHead c0 _ _) +\Rightarrow c0])) in (let TMP_14 \def (Bind b) in (let TMP_15 \def (CHead c1 +TMP_14 u) in (let TMP_16 \def (Bind b) in (let TMP_17 \def (CHead c2 TMP_16 +u) in (let H6 \def (f_equal C C TMP_13 TMP_15 TMP_17 H4) in (let TMP_22 \def +(\lambda (c0: C).((eq C c1 c0) \to (\forall (t3: T).(\forall (t4: T).((ty3 g +c1 t3 t4) \to (let TMP_18 \def (cbk c1) in (let TMP_19 \def (CSort TMP_18) in +(let TMP_20 \def (app1 c1 t3) in (let TMP_21 \def (app1 c1 t4) in (ty3 g +TMP_19 TMP_20 TMP_21)))))))))) in (let H7 \def (eq_ind_r C c2 TMP_22 H2 c1 +H6) in (let TMP_23 \def (\lambda (c0: C).(wf3 g c1 c0)) in (let H8 \def +(eq_ind_r C c2 TMP_23 H1 c1 H6) in (let TMP_26 \def (\lambda (t0: T).(let +TMP_24 \def (Bind b) in (let TMP_25 \def (CHead c1 TMP_24 u) in (ty3 g TMP_25 +t2 t0)))) in (let TMP_27 \def (cbk c1) in (let TMP_28 \def (CSort TMP_27) in +(let TMP_29 \def (Bind b) in (let TMP_30 \def (THead TMP_29 u t1) in (let +TMP_31 \def (app1 c1 TMP_30) in (let TMP_32 \def (Bind b) in (let TMP_33 \def +(THead TMP_32 u t2) in (let TMP_34 \def (app1 c1 TMP_33) in (let TMP_35 \def +(ty3 g TMP_28 TMP_31 TMP_34) in (let TMP_42 \def (\lambda (x: T).(\lambda (_: +(ty3 g (CHead c1 (Bind b) u) t2 x)).(let TMP_36 \def (refl_equal C c1) in +(let TMP_37 \def (Bind b) in (let TMP_38 \def (THead TMP_37 u t1) in (let +TMP_39 \def (Bind b) in (let TMP_40 \def (THead TMP_39 u t2) in (let TMP_41 +\def (ty3_bind g c1 u t H3 b t1 t2 H5) in (H7 TMP_36 TMP_38 TMP_40 +TMP_41))))))))) in (let TMP_43 \def (Bind b) in (let TMP_44 \def (CHead c1 +TMP_43 u) in (let TMP_45 \def (ty3_correct g TMP_44 t1 t2 H5) in (ex_ind T +TMP_26 TMP_35 TMP_42 TMP_45))))))))))))))))))))))))))))))))))))) in (let +TMP_139 \def (\lambda (c1: C).(\lambda (c2: C).(\lambda (H1: (wf3 g c1 +c2)).(\lambda (H2: (((eq C c1 c2) \to (\forall (t1: T).(\forall (t2: T).((ty3 +g c1 t1 t2) \to (ty3 g (CSort (cbk c1)) (app1 c1 t1) (app1 c1 +t2)))))))).(\lambda (u: T).(\lambda (H3: ((\forall (t: T).((ty3 g c1 u t) \to +False)))).(\lambda (b: B).(\lambda (H4: (eq C (CHead c1 (Bind b) u) (CHead c2 +(Bind Void) (TSort O)))).(\lambda (t1: T).(\lambda (t2: T).(\lambda (H5: (ty3 +g (CHead c1 (Bind b) u) t1 t2)).(let TMP_47 \def (\lambda (e: C).(match e +with [(CSort _) \Rightarrow c1 | (CHead c0 _ _) \Rightarrow c0])) in (let +TMP_48 \def (Bind b) in (let TMP_49 \def (CHead c1 TMP_48 u) in (let TMP_50 +\def (Bind Void) in (let TMP_51 \def (TSort O) in (let TMP_52 \def (CHead c2 +TMP_50 TMP_51) in (let H6 \def (f_equal C C TMP_47 TMP_49 TMP_52 H4) in (let +TMP_53 \def (\lambda (e: C).(match e with [(CSort _) \Rightarrow b | (CHead _ +k _) \Rightarrow (match k with [(Bind b0) \Rightarrow b0 | (Flat _) +\Rightarrow b])])) in (let TMP_54 \def (Bind b) in (let TMP_55 \def (CHead c1 +TMP_54 u) in (let TMP_56 \def (Bind Void) in (let TMP_57 \def (TSort O) in +(let TMP_58 \def (CHead c2 TMP_56 TMP_57) in (let H7 \def (f_equal C B TMP_53 +TMP_55 TMP_58 H4) in (let TMP_59 \def (\lambda (e: C).(match e with [(CSort +_) \Rightarrow u | (CHead _ _ t) \Rightarrow t])) in (let TMP_60 \def (Bind +b) in (let TMP_61 \def (CHead c1 TMP_60 u) in (let TMP_62 \def (Bind Void) in +(let TMP_63 \def (TSort O) in (let TMP_64 \def (CHead c2 TMP_62 TMP_63) in +(let H8 \def (f_equal C T TMP_59 TMP_61 TMP_64 H4) in (let TMP_137 \def +(\lambda (H9: (eq B b Void)).(\lambda (H10: (eq C c1 c2)).(let TMP_67 \def +(\lambda (b0: B).(let TMP_65 \def (Bind b0) in (let TMP_66 \def (CHead c1 +TMP_65 u) in (ty3 g TMP_66 t1 t2)))) in (let H11 \def (eq_ind B b TMP_67 H5 +Void H9) in (let TMP_78 \def (\lambda (b0: B).(let TMP_68 \def (Bind b0) in +(let TMP_69 \def (CHead c1 TMP_68 u) in (let TMP_70 \def (cbk TMP_69) in (let +TMP_71 \def (CSort TMP_70) in (let TMP_72 \def (Bind b0) in (let TMP_73 \def +(CHead c1 TMP_72 u) in (let TMP_74 \def (app1 TMP_73 t1) in (let TMP_75 \def +(Bind b0) in (let TMP_76 \def (CHead c1 TMP_75 u) in (let TMP_77 \def (app1 +TMP_76 t2) in (ty3 g TMP_71 TMP_74 TMP_77)))))))))))) in (let TMP_81 \def +(\lambda (t: T).(let TMP_79 \def (Bind Void) in (let TMP_80 \def (CHead c1 +TMP_79 t) in (ty3 g TMP_80 t1 t2)))) in (let TMP_82 \def (TSort O) in (let +H12 \def (eq_ind T u TMP_81 H11 TMP_82 H8) in (let TMP_83 \def (\lambda (t: +T).(\forall (t0: T).((ty3 g c1 t t0) \to False))) in (let TMP_84 \def (TSort +O) in (let H13 \def (eq_ind T u TMP_83 H3 TMP_84 H8) in (let TMP_85 \def +(TSort O) in (let TMP_96 \def (\lambda (t: T).(let TMP_86 \def (Bind Void) in +(let TMP_87 \def (CHead c1 TMP_86 t) in (let TMP_88 \def (cbk TMP_87) in (let +TMP_89 \def (CSort TMP_88) in (let TMP_90 \def (Bind Void) in (let TMP_91 +\def (CHead c1 TMP_90 t) in (let TMP_92 \def (app1 TMP_91 t1) in (let TMP_93 +\def (Bind Void) in (let TMP_94 \def (CHead c1 TMP_93 t) in (let TMP_95 \def +(app1 TMP_94 t2) in (ty3 g TMP_89 TMP_92 TMP_95)))))))))))) in (let TMP_101 +\def (\lambda (c0: C).((eq C c1 c0) \to (\forall (t3: T).(\forall (t4: +T).((ty3 g c1 t3 t4) \to (let TMP_97 \def (cbk c1) in (let TMP_98 \def (CSort +TMP_97) in (let TMP_99 \def (app1 c1 t3) in (let TMP_100 \def (app1 c1 t4) in +(ty3 g TMP_98 TMP_99 TMP_100)))))))))) in (let H14 \def (eq_ind_r C c2 +TMP_101 H2 c1 H10) in (let TMP_102 \def (\lambda (c0: C).(wf3 g c1 c0)) in +(let H15 \def (eq_ind_r C c2 TMP_102 H1 c1 H10) in (let TMP_106 \def (\lambda +(t: T).(let TMP_103 \def (Bind Void) in (let TMP_104 \def (TSort O) in (let +TMP_105 \def (CHead c1 TMP_103 TMP_104) in (ty3 g TMP_105 t2 t))))) in (let +TMP_107 \def (cbk c1) in (let TMP_108 \def (CSort TMP_107) in (let TMP_109 +\def (Bind Void) in (let TMP_110 \def (TSort O) in (let TMP_111 \def (THead +TMP_109 TMP_110 t1) in (let TMP_112 \def (app1 c1 TMP_111) in (let TMP_113 +\def (Bind Void) in (let TMP_114 \def (TSort O) in (let TMP_115 \def (THead +TMP_113 TMP_114 t2) in (let TMP_116 \def (app1 c1 TMP_115) in (let TMP_117 +\def (ty3 g TMP_108 TMP_112 TMP_116) in (let TMP_130 \def (\lambda (x: +T).(\lambda (_: (ty3 g (CHead c1 (Bind Void) (TSort O)) t2 x)).(let TMP_118 +\def (refl_equal C c1) in (let TMP_119 \def (Bind Void) in (let TMP_120 \def +(TSort O) in (let TMP_121 \def (THead TMP_119 TMP_120 t1) in (let TMP_122 +\def (Bind Void) in (let TMP_123 \def (TSort O) in (let TMP_124 \def (THead +TMP_122 TMP_123 t2) in (let TMP_125 \def (TSort O) in (let TMP_126 \def (next +g O) in (let TMP_127 \def (TSort TMP_126) in (let TMP_128 \def (ty3_sort g c1 +O) in (let TMP_129 \def (ty3_bind g c1 TMP_125 TMP_127 TMP_128 Void t1 t2 +H12) in (H14 TMP_118 TMP_121 TMP_124 TMP_129))))))))))))))) in (let TMP_131 +\def (Bind Void) in (let TMP_132 \def (TSort O) in (let TMP_133 \def (CHead +c1 TMP_131 TMP_132) in (let TMP_134 \def (ty3_correct g TMP_133 t1 t2 H12) in +(let TMP_135 \def (ex_ind T TMP_106 TMP_117 TMP_130 TMP_134) in (let TMP_136 +\def (eq_ind_r T TMP_85 TMP_96 TMP_135 u H8) in (eq_ind_r B Void TMP_78 +TMP_136 b H9))))))))))))))))))))))))))))))))))))) in (let TMP_138 \def +(TMP_137 H7) in (TMP_138 H6))))))))))))))))))))))))))))))))))) in (let +TMP_179 \def (\lambda (c1: C).(\lambda (c2: C).(\lambda (H1: (wf3 g c1 +c2)).(\lambda (H2: (((eq C c1 c2) \to (\forall (t1: T).(\forall (t2: T).((ty3 +g c1 t1 t2) \to (ty3 g (CSort (cbk c1)) (app1 c1 t1) (app1 c1 t2)))))))).(\lambda (u: T).(\lambda (f: F).(\lambda (H3: (eq C (CHead c1 (Flat f) u) c2)).(\lambda (t1: T).(\lambda (t2: T).(\lambda (_: (ty3 g (CHead -c1 (Flat f) u) t1 t2)).(let H5 \def (f_equal C C (\lambda (e: C).e) (CHead c1 -(Flat f) u) c2 H3) in (let H6 \def (eq_ind_r C c2 (\lambda (c0: C).((eq C c1 -c0) \to (\forall (t3: T).(\forall (t4: T).((ty3 g c1 t3 t4) \to (ty3 g (CSort -(cbk c1)) (app1 c1 t3) (app1 c1 t4))))))) H2 (CHead c1 (Flat f) u) H5) in -(let H7 \def (eq_ind_r C c2 (\lambda (c0: C).(wf3 g c1 c0)) H1 (CHead c1 -(Flat f) u) H5) in (let H_x \def (wf3_gen_head2 g c1 c1 u (Flat f) H7) in -(let H8 \def H_x in (ex_ind B (\lambda (b: B).(eq K (Flat f) (Bind b))) (ty3 -g (CSort (cbk c1)) (app1 c1 (THead (Flat f) u t1)) (app1 c1 (THead (Flat f) u -t2))) (\lambda (x: B).(\lambda (H9: (eq K (Flat f) (Bind x))).(let H10 \def -(eq_ind K (Flat f) (\lambda (ee: K).(match ee in K return (\lambda (_: -K).Prop) with [(Bind _) \Rightarrow False | (Flat _) \Rightarrow True])) I -(Bind x) H9) in (False_ind (ty3 g (CSort (cbk c1)) (app1 c1 (THead (Flat f) u -t1)) (app1 c1 (THead (Flat f) u t2))) H10)))) H8)))))))))))))))) y c H0))) -H))). -(* COMMENTS -Initial nodes: 1677 -END *) +c1 (Flat f) u) t1 t2)).(let TMP_140 \def (\lambda (e: C).e) in (let TMP_141 +\def (Flat f) in (let TMP_142 \def (CHead c1 TMP_141 u) in (let H5 \def +(f_equal C C TMP_140 TMP_142 c2 H3) in (let TMP_147 \def (\lambda (c0: +C).((eq C c1 c0) \to (\forall (t3: T).(\forall (t4: T).((ty3 g c1 t3 t4) \to +(let TMP_143 \def (cbk c1) in (let TMP_144 \def (CSort TMP_143) in (let +TMP_145 \def (app1 c1 t3) in (let TMP_146 \def (app1 c1 t4) in (ty3 g TMP_144 +TMP_145 TMP_146)))))))))) in (let TMP_148 \def (Flat f) in (let TMP_149 \def +(CHead c1 TMP_148 u) in (let H6 \def (eq_ind_r C c2 TMP_147 H2 TMP_149 H5) in +(let TMP_150 \def (\lambda (c0: C).(wf3 g c1 c0)) in (let TMP_151 \def (Flat +f) in (let TMP_152 \def (CHead c1 TMP_151 u) in (let H7 \def (eq_ind_r C c2 +TMP_150 H1 TMP_152 H5) in (let TMP_153 \def (Flat f) in (let H_x \def +(wf3_gen_head2 g c1 c1 u TMP_153 H7) in (let H8 \def H_x in (let TMP_156 \def +(\lambda (b: B).(let TMP_154 \def (Flat f) in (let TMP_155 \def (Bind b) in +(eq K TMP_154 TMP_155)))) in (let TMP_157 \def (cbk c1) in (let TMP_158 \def +(CSort TMP_157) in (let TMP_159 \def (Flat f) in (let TMP_160 \def (THead +TMP_159 u t1) in (let TMP_161 \def (app1 c1 TMP_160) in (let TMP_162 \def +(Flat f) in (let TMP_163 \def (THead TMP_162 u t2) in (let TMP_164 \def (app1 +c1 TMP_163) in (let TMP_165 \def (ty3 g TMP_158 TMP_161 TMP_164) in (let +TMP_178 \def (\lambda (x: B).(\lambda (H9: (eq K (Flat f) (Bind x))).(let +TMP_166 \def (Flat f) in (let TMP_167 \def (\lambda (ee: K).(match ee with +[(Bind _) \Rightarrow False | (Flat _) \Rightarrow True])) in (let TMP_168 +\def (Bind x) in (let H10 \def (eq_ind K TMP_166 TMP_167 I TMP_168 H9) in +(let TMP_169 \def (cbk c1) in (let TMP_170 \def (CSort TMP_169) in (let +TMP_171 \def (Flat f) in (let TMP_172 \def (THead TMP_171 u t1) in (let +TMP_173 \def (app1 c1 TMP_172) in (let TMP_174 \def (Flat f) in (let TMP_175 +\def (THead TMP_174 u t2) in (let TMP_176 \def (app1 c1 TMP_175) in (let +TMP_177 \def (ty3 g TMP_170 TMP_173 TMP_176) in (False_ind TMP_177 +H10)))))))))))))))) in (ex_ind B TMP_156 TMP_165 TMP_178 +H8))))))))))))))))))))))))))))))))))))) in (wf3_ind g TMP_11 TMP_12 TMP_46 +TMP_139 TMP_179 y c H0)))))))) in (insert_eq C c TMP_1 TMP_6 TMP_180 H)))))). theorem wf3_idem: \forall (g: G).(\forall (c1: C).(\forall (c2: C).((wf3 g c1 c2) \to (wf3 g c2 c2)))) \def \lambda (g: G).(\lambda (c1: C).(\lambda (c2: C).(\lambda (H: (wf3 g c1 -c2)).(wf3_ind g (\lambda (_: C).(\lambda (c0: C).(wf3 g c0 c0))) (\lambda (m: -nat).(wf3_sort g m)) (\lambda (c3: C).(\lambda (c4: C).(\lambda (H0: (wf3 g -c3 c4)).(\lambda (H1: (wf3 g c4 c4)).(\lambda (u: T).(\lambda (t: T).(\lambda -(H2: (ty3 g c3 u t)).(\lambda (b: B).(wf3_bind g c4 c4 H1 u t (wf3_ty3_conf g -c3 u t H2 c4 H0) b))))))))) (\lambda (c3: C).(\lambda (c4: C).(\lambda (_: -(wf3 g c3 c4)).(\lambda (H1: (wf3 g c4 c4)).(\lambda (u: T).(\lambda (_: -((\forall (t: T).((ty3 g c3 u t) \to False)))).(\lambda (_: B).(wf3_bind g c4 -c4 H1 (TSort O) (TSort (next g O)) (ty3_sort g c4 O) Void)))))))) (\lambda -(c3: C).(\lambda (c4: C).(\lambda (_: (wf3 g c3 c4)).(\lambda (H1: (wf3 g c4 -c4)).(\lambda (_: T).(\lambda (_: F).H1)))))) c1 c2 H)))). -(* COMMENTS -Initial nodes: 207 -END *) +c2)).(let TMP_1 \def (\lambda (_: C).(\lambda (c0: C).(wf3 g c0 c0))) in (let +TMP_2 \def (\lambda (m: nat).(wf3_sort g m)) in (let TMP_4 \def (\lambda (c3: +C).(\lambda (c4: C).(\lambda (H0: (wf3 g c3 c4)).(\lambda (H1: (wf3 g c4 +c4)).(\lambda (u: T).(\lambda (t: T).(\lambda (H2: (ty3 g c3 u t)).(\lambda +(b: B).(let TMP_3 \def (wf3_ty3_conf g c3 u t H2 c4 H0) in (wf3_bind g c4 c4 +H1 u t TMP_3 b)))))))))) in (let TMP_9 \def (\lambda (c3: C).(\lambda (c4: +C).(\lambda (_: (wf3 g c3 c4)).(\lambda (H1: (wf3 g c4 c4)).(\lambda (u: +T).(\lambda (_: ((\forall (t: T).((ty3 g c3 u t) \to False)))).(\lambda (_: +B).(let TMP_5 \def (TSort O) in (let TMP_6 \def (next g O) in (let TMP_7 \def +(TSort TMP_6) in (let TMP_8 \def (ty3_sort g c4 O) in (wf3_bind g c4 c4 H1 +TMP_5 TMP_7 TMP_8 Void)))))))))))) in (let TMP_10 \def (\lambda (c3: +C).(\lambda (c4: C).(\lambda (_: (wf3 g c3 c4)).(\lambda (H1: (wf3 g c4 +c4)).(\lambda (_: T).(\lambda (_: F).H1)))))) in (wf3_ind g TMP_1 TMP_2 TMP_4 +TMP_9 TMP_10 c1 c2 H))))))))). theorem wf3_ty3: \forall (g: G).(\forall (c1: C).(\forall (t: T).(\forall (u: T).((ty3 g c1 t @@ -237,12 +236,12 @@ u) \to (ex2 C (\lambda (c2: C).(wf3 g c1 c2)) (\lambda (c2: C).(ty3 g c2 t u))))))) \def \lambda (g: G).(\lambda (c1: C).(\lambda (t: T).(\lambda (u: T).(\lambda (H: -(ty3 g c1 t u)).(let H_x \def (wf3_total g c1) in (let H0 \def H_x in (ex_ind -C (\lambda (c2: C).(wf3 g c1 c2)) (ex2 C (\lambda (c2: C).(wf3 g c1 c2)) -(\lambda (c2: C).(ty3 g c2 t u))) (\lambda (x: C).(\lambda (H1: (wf3 g c1 -x)).(ex_intro2 C (\lambda (c2: C).(wf3 g c1 c2)) (\lambda (c2: C).(ty3 g c2 t -u)) x H1 (wf3_ty3_conf g c1 t u H x H1)))) H0))))))). -(* COMMENTS -Initial nodes: 123 -END *) +(ty3 g c1 t u)).(let H_x \def (wf3_total g c1) in (let H0 \def H_x in (let +TMP_1 \def (\lambda (c2: C).(wf3 g c1 c2)) in (let TMP_2 \def (\lambda (c2: +C).(wf3 g c1 c2)) in (let TMP_3 \def (\lambda (c2: C).(ty3 g c2 t u)) in (let +TMP_4 \def (ex2 C TMP_2 TMP_3) in (let TMP_8 \def (\lambda (x: C).(\lambda +(H1: (wf3 g c1 x)).(let TMP_5 \def (\lambda (c2: C).(wf3 g c1 c2)) in (let +TMP_6 \def (\lambda (c2: C).(ty3 g c2 t u)) in (let TMP_7 \def (wf3_ty3_conf +g c1 t u H x H1) in (ex_intro2 C TMP_5 TMP_6 x H1 TMP_7)))))) in (ex_ind C +TMP_1 TMP_4 TMP_8 H0)))))))))))). diff --git a/matita/matita/contribs/lambdadelta/basic_1/wf3/ty3.ma b/matita/matita/contribs/lambdadelta/basic_1/wf3/ty3.ma index e47d4a2e0..70dc78087 100644 --- a/matita/matita/contribs/lambdadelta/basic_1/wf3/ty3.ma +++ b/matita/matita/contribs/lambdadelta/basic_1/wf3/ty3.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -include "Basic-1/wf3/getl.ma". +include "basic_1/wf3/getl.ma". theorem wf3_pr2_conf: \forall (g: G).(\forall (c1: C).(\forall (t1: T).(\forall (t2: T).((pr2 c1 @@ -22,27 +22,28 @@ t1 t2) \to (\forall (c2: C).((wf3 g c1 c2) \to (\forall (u: T).((ty3 g c1 t1 u) \to (pr2 c2 t1 t2))))))))) \def \lambda (g: G).(\lambda (c1: C).(\lambda (t1: T).(\lambda (t2: T).(\lambda -(H: (pr2 c1 t1 t2)).(pr2_ind (\lambda (c: C).(\lambda (t: T).(\lambda (t0: -T).(\forall (c2: C).((wf3 g c c2) \to (\forall (u: T).((ty3 g c t u) \to (pr2 -c2 t t0)))))))) (\lambda (c: C).(\lambda (t3: T).(\lambda (t4: T).(\lambda -(H0: (pr0 t3 t4)).(\lambda (c2: C).(\lambda (_: (wf3 g c c2)).(\lambda (u: -T).(\lambda (_: (ty3 g c t3 u)).(pr2_free c2 t3 t4 H0))))))))) (\lambda (c: -C).(\lambda (d: C).(\lambda (u: T).(\lambda (i: nat).(\lambda (H0: (getl i c -(CHead d (Bind Abbr) u))).(\lambda (t3: T).(\lambda (t4: T).(\lambda (H1: -(pr0 t3 t4)).(\lambda (t: T).(\lambda (H2: (subst0 i u t4 t)).(\lambda (c2: -C).(\lambda (H3: (wf3 g c c2)).(\lambda (u0: T).(\lambda (H4: (ty3 g c t3 -u0)).(let H_y \def (ty3_sred_pr0 t3 t4 H1 g c u0 H4) in (let H_x \def -(ty3_getl_subst0 g c t4 u0 H_y u t i H2 Abbr d u H0) in (let H5 \def H_x in -(ex_ind T (\lambda (w: T).(ty3 g d u w)) (pr2 c2 t3 t) (\lambda (x: -T).(\lambda (H6: (ty3 g d u x)).(let H_x0 \def (wf3_getl_conf Abbr i c d u H0 -g c2 H3 x H6) in (let H7 \def H_x0 in (ex2_ind C (\lambda (d2: C).(getl i c2 -(CHead d2 (Bind Abbr) u))) (\lambda (d2: C).(wf3 g d d2)) (pr2 c2 t3 t) -(\lambda (x0: C).(\lambda (H8: (getl i c2 (CHead x0 (Bind Abbr) u))).(\lambda -(_: (wf3 g d x0)).(pr2_delta c2 x0 u i H8 t3 t4 H1 t H2)))) H7))))) -H5)))))))))))))))))) c1 t1 t2 H))))). -(* COMMENTS -Initial nodes: 373 -END *) +(H: (pr2 c1 t1 t2)).(let TMP_1 \def (\lambda (c: C).(\lambda (t: T).(\lambda +(t0: T).(\forall (c2: C).((wf3 g c c2) \to (\forall (u: T).((ty3 g c t u) \to +(pr2 c2 t t0)))))))) in (let TMP_2 \def (\lambda (c: C).(\lambda (t3: +T).(\lambda (t4: T).(\lambda (H0: (pr0 t3 t4)).(\lambda (c2: C).(\lambda (_: +(wf3 g c c2)).(\lambda (u: T).(\lambda (_: (ty3 g c t3 u)).(pr2_free c2 t3 t4 +H0))))))))) in (let TMP_12 \def (\lambda (c: C).(\lambda (d: C).(\lambda (u: +T).(\lambda (i: nat).(\lambda (H0: (getl i c (CHead d (Bind Abbr) +u))).(\lambda (t3: T).(\lambda (t4: T).(\lambda (H1: (pr0 t3 t4)).(\lambda +(t: T).(\lambda (H2: (subst0 i u t4 t)).(\lambda (c2: C).(\lambda (H3: (wf3 g +c c2)).(\lambda (u0: T).(\lambda (H4: (ty3 g c t3 u0)).(let H_y \def +(ty3_sred_pr0 t3 t4 H1 g c u0 H4) in (let H_x \def (ty3_getl_subst0 g c t4 u0 +H_y u t i H2 Abbr d u H0) in (let H5 \def H_x in (let TMP_3 \def (\lambda (w: +T).(ty3 g d u w)) in (let TMP_4 \def (pr2 c2 t3 t) in (let TMP_11 \def +(\lambda (x: T).(\lambda (H6: (ty3 g d u x)).(let H_x0 \def (wf3_getl_conf +Abbr i c d u H0 g c2 H3 x H6) in (let H7 \def H_x0 in (let TMP_7 \def +(\lambda (d2: C).(let TMP_5 \def (Bind Abbr) in (let TMP_6 \def (CHead d2 +TMP_5 u) in (getl i c2 TMP_6)))) in (let TMP_8 \def (\lambda (d2: C).(wf3 g d +d2)) in (let TMP_9 \def (pr2 c2 t3 t) in (let TMP_10 \def (\lambda (x0: +C).(\lambda (H8: (getl i c2 (CHead x0 (Bind Abbr) u))).(\lambda (_: (wf3 g d +x0)).(pr2_delta c2 x0 u i H8 t3 t4 H1 t H2)))) in (ex2_ind C TMP_7 TMP_8 +TMP_9 TMP_10 H7))))))))) in (ex_ind T TMP_3 TMP_4 TMP_11 +H5))))))))))))))))))))) in (pr2_ind TMP_1 TMP_2 TMP_12 c1 t1 t2 H)))))))). theorem wf3_pr3_conf: \forall (g: G).(\forall (c1: C).(\forall (t1: T).(\forall (t2: T).((pr3 c1 @@ -50,19 +51,18 @@ t1 t2) \to (\forall (c2: C).((wf3 g c1 c2) \to (\forall (u: T).((ty3 g c1 t1 u) \to (pr3 c2 t1 t2))))))))) \def \lambda (g: G).(\lambda (c1: C).(\lambda (t1: T).(\lambda (t2: T).(\lambda -(H: (pr3 c1 t1 t2)).(pr3_ind c1 (\lambda (t: T).(\lambda (t0: T).(\forall +(H: (pr3 c1 t1 t2)).(let TMP_1 \def (\lambda (t: T).(\lambda (t0: T).(\forall (c2: C).((wf3 g c1 c2) \to (\forall (u: T).((ty3 g c1 t u) \to (pr3 c2 t -t0))))))) (\lambda (t: T).(\lambda (c2: C).(\lambda (_: (wf3 g c1 -c2)).(\lambda (u: T).(\lambda (_: (ty3 g c1 t u)).(pr3_refl c2 t)))))) -(\lambda (t3: T).(\lambda (t4: T).(\lambda (H0: (pr2 c1 t4 t3)).(\lambda (t5: -T).(\lambda (_: (pr3 c1 t3 t5)).(\lambda (H2: ((\forall (c2: C).((wf3 g c1 -c2) \to (\forall (u: T).((ty3 g c1 t3 u) \to (pr3 c2 t3 t5))))))).(\lambda -(c2: C).(\lambda (H3: (wf3 g c1 c2)).(\lambda (u: T).(\lambda (H4: (ty3 g c1 -t4 u)).(pr3_sing c2 t3 t4 (wf3_pr2_conf g c1 t4 t3 H0 c2 H3 u H4) t5 (H2 c2 -H3 u (ty3_sred_pr2 c1 t4 t3 H0 g u H4))))))))))))) t1 t2 H))))). -(* COMMENTS -Initial nodes: 217 -END *) +t0))))))) in (let TMP_2 \def (\lambda (t: T).(\lambda (c2: C).(\lambda (_: +(wf3 g c1 c2)).(\lambda (u: T).(\lambda (_: (ty3 g c1 t u)).(pr3_refl c2 +t)))))) in (let TMP_6 \def (\lambda (t3: T).(\lambda (t4: T).(\lambda (H0: +(pr2 c1 t4 t3)).(\lambda (t5: T).(\lambda (_: (pr3 c1 t3 t5)).(\lambda (H2: +((\forall (c2: C).((wf3 g c1 c2) \to (\forall (u: T).((ty3 g c1 t3 u) \to +(pr3 c2 t3 t5))))))).(\lambda (c2: C).(\lambda (H3: (wf3 g c1 c2)).(\lambda +(u: T).(\lambda (H4: (ty3 g c1 t4 u)).(let TMP_3 \def (wf3_pr2_conf g c1 t4 +t3 H0 c2 H3 u H4) in (let TMP_4 \def (ty3_sred_pr2 c1 t4 t3 H0 g u H4) in +(let TMP_5 \def (H2 c2 H3 u TMP_4) in (pr3_sing c2 t3 t4 TMP_3 t5 +TMP_5)))))))))))))) in (pr3_ind c1 TMP_1 TMP_2 TMP_6 t1 t2 H)))))))). theorem wf3_pc3_conf: \forall (g: G).(\forall (c1: C).(\forall (t1: T).(\forall (t2: T).((pc3 c1 @@ -72,67 +72,79 @@ u1) \to (\forall (u2: T).((ty3 g c1 t2 u2) \to (pc3 c2 t1 t2))))))))))) \lambda (g: G).(\lambda (c1: C).(\lambda (t1: T).(\lambda (t2: T).(\lambda (H: (pc3 c1 t1 t2)).(\lambda (c2: C).(\lambda (H0: (wf3 g c1 c2)).(\lambda (u1: T).(\lambda (H1: (ty3 g c1 t1 u1)).(\lambda (u2: T).(\lambda (H2: (ty3 g -c1 t2 u2)).(let H3 \def H in (ex2_ind T (\lambda (t: T).(pr3 c1 t1 t)) -(\lambda (t: T).(pr3 c1 t2 t)) (pc3 c2 t1 t2) (\lambda (x: T).(\lambda (H4: -(pr3 c1 t1 x)).(\lambda (H5: (pr3 c1 t2 x)).(pc3_pr3_t c2 t1 x (wf3_pr3_conf -g c1 t1 x H4 c2 H0 u1 H1) t2 (wf3_pr3_conf g c1 t2 x H5 c2 H0 u2 H2))))) -H3)))))))))))). -(* COMMENTS -Initial nodes: 153 -END *) +c1 t2 u2)).(let H3 \def H in (let TMP_1 \def (\lambda (t: T).(pr3 c1 t1 t)) +in (let TMP_2 \def (\lambda (t: T).(pr3 c1 t2 t)) in (let TMP_3 \def (pc3 c2 +t1 t2) in (let TMP_6 \def (\lambda (x: T).(\lambda (H4: (pr3 c1 t1 +x)).(\lambda (H5: (pr3 c1 t2 x)).(let TMP_4 \def (wf3_pr3_conf g c1 t1 x H4 +c2 H0 u1 H1) in (let TMP_5 \def (wf3_pr3_conf g c1 t2 x H5 c2 H0 u2 H2) in +(pc3_pr3_t c2 t1 x TMP_4 t2 TMP_5)))))) in (ex2_ind T TMP_1 TMP_2 TMP_3 TMP_6 +H3)))))))))))))))). theorem wf3_ty3_conf: \forall (g: G).(\forall (c1: C).(\forall (t1: T).(\forall (t2: T).((ty3 g c1 t1 t2) \to (\forall (c2: C).((wf3 g c1 c2) \to (ty3 g c2 t1 t2))))))) \def \lambda (g: G).(\lambda (c1: C).(\lambda (t1: T).(\lambda (t2: T).(\lambda -(H: (ty3 g c1 t1 t2)).(ty3_ind g (\lambda (c: C).(\lambda (t: T).(\lambda -(t0: T).(\forall (c2: C).((wf3 g c c2) \to (ty3 g c2 t t0)))))) (\lambda (c: -C).(\lambda (t3: T).(\lambda (t: T).(\lambda (H0: (ty3 g c t3 t)).(\lambda -(H1: ((\forall (c2: C).((wf3 g c c2) \to (ty3 g c2 t3 t))))).(\lambda (u: -T).(\lambda (t4: T).(\lambda (H2: (ty3 g c u t4)).(\lambda (H3: ((\forall -(c2: C).((wf3 g c c2) \to (ty3 g c2 u t4))))).(\lambda (H4: (pc3 c t4 -t3)).(\lambda (c2: C).(\lambda (H5: (wf3 g c c2)).(ex_ind T (\lambda (t0: -T).(ty3 g c t4 t0)) (ty3 g c2 u t3) (\lambda (x: T).(\lambda (H6: (ty3 g c t4 -x)).(ty3_conv g c2 t3 t (H1 c2 H5) u t4 (H3 c2 H5) (wf3_pc3_conf g c t4 t3 H4 -c2 H5 x H6 t H0)))) (ty3_correct g c u t4 H2)))))))))))))) (\lambda (c: -C).(\lambda (m: nat).(\lambda (c2: C).(\lambda (_: (wf3 g c c2)).(ty3_sort g -c2 m))))) (\lambda (n: nat).(\lambda (c: C).(\lambda (d: C).(\lambda (u: -T).(\lambda (H0: (getl n c (CHead d (Bind Abbr) u))).(\lambda (t: T).(\lambda +(H: (ty3 g c1 t1 t2)).(let TMP_1 \def (\lambda (c: C).(\lambda (t: +T).(\lambda (t0: T).(\forall (c2: C).((wf3 g c c2) \to (ty3 g c2 t t0)))))) +in (let TMP_9 \def (\lambda (c: C).(\lambda (t3: T).(\lambda (t: T).(\lambda +(H0: (ty3 g c t3 t)).(\lambda (H1: ((\forall (c2: C).((wf3 g c c2) \to (ty3 g +c2 t3 t))))).(\lambda (u: T).(\lambda (t4: T).(\lambda (H2: (ty3 g c u +t4)).(\lambda (H3: ((\forall (c2: C).((wf3 g c c2) \to (ty3 g c2 u +t4))))).(\lambda (H4: (pc3 c t4 t3)).(\lambda (c2: C).(\lambda (H5: (wf3 g c +c2)).(let TMP_2 \def (\lambda (t0: T).(ty3 g c t4 t0)) in (let TMP_3 \def +(ty3 g c2 u t3) in (let TMP_7 \def (\lambda (x: T).(\lambda (H6: (ty3 g c t4 +x)).(let TMP_4 \def (H1 c2 H5) in (let TMP_5 \def (H3 c2 H5) in (let TMP_6 +\def (wf3_pc3_conf g c t4 t3 H4 c2 H5 x H6 t H0) in (ty3_conv g c2 t3 t TMP_4 +u t4 TMP_5 TMP_6)))))) in (let TMP_8 \def (ty3_correct g c u t4 H2) in +(ex_ind T TMP_2 TMP_3 TMP_7 TMP_8))))))))))))))))) in (let TMP_10 \def +(\lambda (c: C).(\lambda (m: nat).(\lambda (c2: C).(\lambda (_: (wf3 g c +c2)).(ty3_sort g c2 m))))) in (let TMP_21 \def (\lambda (n: nat).(\lambda (c: +C).(\lambda (d: C).(\lambda (u: T).(\lambda (H0: (getl n c (CHead d (Bind +Abbr) u))).(\lambda (t: T).(\lambda (H1: (ty3 g d u t)).(\lambda (H2: +((\forall (c2: C).((wf3 g d c2) \to (ty3 g c2 u t))))).(\lambda (c2: +C).(\lambda (H3: (wf3 g c c2)).(let H_x \def (wf3_getl_conf Abbr n c d u H0 g +c2 H3 t H1) in (let H4 \def H_x in (let TMP_13 \def (\lambda (d2: C).(let +TMP_11 \def (Bind Abbr) in (let TMP_12 \def (CHead d2 TMP_11 u) in (getl n c2 +TMP_12)))) in (let TMP_14 \def (\lambda (d2: C).(wf3 g d d2)) in (let TMP_15 +\def (TLRef n) in (let TMP_16 \def (S n) in (let TMP_17 \def (lift TMP_16 O +t) in (let TMP_18 \def (ty3 g c2 TMP_15 TMP_17) in (let TMP_20 \def (\lambda +(x: C).(\lambda (H5: (getl n c2 (CHead x (Bind Abbr) u))).(\lambda (H6: (wf3 +g d x)).(let TMP_19 \def (H2 x H6) in (ty3_abbr g n c2 x u H5 t TMP_19))))) +in (ex2_ind C TMP_13 TMP_14 TMP_18 TMP_20 H4)))))))))))))))))))) in (let +TMP_32 \def (\lambda (n: nat).(\lambda (c: C).(\lambda (d: C).(\lambda (u: +T).(\lambda (H0: (getl n c (CHead d (Bind Abst) u))).(\lambda (t: T).(\lambda (H1: (ty3 g d u t)).(\lambda (H2: ((\forall (c2: C).((wf3 g d c2) \to (ty3 g c2 u t))))).(\lambda (c2: C).(\lambda (H3: (wf3 g c c2)).(let H_x \def -(wf3_getl_conf Abbr n c d u H0 g c2 H3 t H1) in (let H4 \def H_x in (ex2_ind -C (\lambda (d2: C).(getl n c2 (CHead d2 (Bind Abbr) u))) (\lambda (d2: -C).(wf3 g d d2)) (ty3 g c2 (TLRef n) (lift (S n) O t)) (\lambda (x: -C).(\lambda (H5: (getl n c2 (CHead x (Bind Abbr) u))).(\lambda (H6: (wf3 g d -x)).(ty3_abbr g n c2 x u H5 t (H2 x H6))))) H4))))))))))))) (\lambda (n: -nat).(\lambda (c: C).(\lambda (d: C).(\lambda (u: T).(\lambda (H0: (getl n c -(CHead d (Bind Abst) u))).(\lambda (t: T).(\lambda (H1: (ty3 g d u -t)).(\lambda (H2: ((\forall (c2: C).((wf3 g d c2) \to (ty3 g c2 u -t))))).(\lambda (c2: C).(\lambda (H3: (wf3 g c c2)).(let H_x \def -(wf3_getl_conf Abst n c d u H0 g c2 H3 t H1) in (let H4 \def H_x in (ex2_ind -C (\lambda (d2: C).(getl n c2 (CHead d2 (Bind Abst) u))) (\lambda (d2: -C).(wf3 g d d2)) (ty3 g c2 (TLRef n) (lift (S n) O u)) (\lambda (x: -C).(\lambda (H5: (getl n c2 (CHead x (Bind Abst) u))).(\lambda (H6: (wf3 g d -x)).(ty3_abst g n c2 x u H5 t (H2 x H6))))) H4))))))))))))) (\lambda (c: -C).(\lambda (u: T).(\lambda (t: T).(\lambda (H0: (ty3 g c u t)).(\lambda (H1: -((\forall (c2: C).((wf3 g c c2) \to (ty3 g c2 u t))))).(\lambda (b: -B).(\lambda (t3: T).(\lambda (t4: T).(\lambda (_: (ty3 g (CHead c (Bind b) u) -t3 t4)).(\lambda (H3: ((\forall (c2: C).((wf3 g (CHead c (Bind b) u) c2) \to -(ty3 g c2 t3 t4))))).(\lambda (c2: C).(\lambda (H4: (wf3 g c c2)).(ty3_bind g -c2 u t (H1 c2 H4) b t3 t4 (H3 (CHead c2 (Bind b) u) (wf3_bind g c c2 H4 u t -H0 b))))))))))))))) (\lambda (c: C).(\lambda (w: T).(\lambda (u: T).(\lambda -(_: (ty3 g c w u)).(\lambda (H1: ((\forall (c2: C).((wf3 g c c2) \to (ty3 g -c2 w u))))).(\lambda (v: T).(\lambda (t: T).(\lambda (_: (ty3 g c v (THead -(Bind Abst) u t))).(\lambda (H3: ((\forall (c2: C).((wf3 g c c2) \to (ty3 g -c2 v (THead (Bind Abst) u t)))))).(\lambda (c2: C).(\lambda (H4: (wf3 g c -c2)).(ty3_appl g c2 w u (H1 c2 H4) v t (H3 c2 H4))))))))))))) (\lambda (c: +(wf3_getl_conf Abst n c d u H0 g c2 H3 t H1) in (let H4 \def H_x in (let +TMP_24 \def (\lambda (d2: C).(let TMP_22 \def (Bind Abst) in (let TMP_23 \def +(CHead d2 TMP_22 u) in (getl n c2 TMP_23)))) in (let TMP_25 \def (\lambda +(d2: C).(wf3 g d d2)) in (let TMP_26 \def (TLRef n) in (let TMP_27 \def (S n) +in (let TMP_28 \def (lift TMP_27 O u) in (let TMP_29 \def (ty3 g c2 TMP_26 +TMP_28) in (let TMP_31 \def (\lambda (x: C).(\lambda (H5: (getl n c2 (CHead x +(Bind Abst) u))).(\lambda (H6: (wf3 g d x)).(let TMP_30 \def (H2 x H6) in +(ty3_abst g n c2 x u H5 t TMP_30))))) in (ex2_ind C TMP_24 TMP_25 TMP_29 +TMP_31 H4)))))))))))))))))))) in (let TMP_38 \def (\lambda (c: C).(\lambda +(u: T).(\lambda (t: T).(\lambda (H0: (ty3 g c u t)).(\lambda (H1: ((\forall +(c2: C).((wf3 g c c2) \to (ty3 g c2 u t))))).(\lambda (b: B).(\lambda (t3: +T).(\lambda (t4: T).(\lambda (_: (ty3 g (CHead c (Bind b) u) t3 t4)).(\lambda +(H3: ((\forall (c2: C).((wf3 g (CHead c (Bind b) u) c2) \to (ty3 g c2 t3 +t4))))).(\lambda (c2: C).(\lambda (H4: (wf3 g c c2)).(let TMP_33 \def (H1 c2 +H4) in (let TMP_34 \def (Bind b) in (let TMP_35 \def (CHead c2 TMP_34 u) in +(let TMP_36 \def (wf3_bind g c c2 H4 u t H0 b) in (let TMP_37 \def (H3 TMP_35 +TMP_36) in (ty3_bind g c2 u t TMP_33 b t3 t4 TMP_37)))))))))))))))))) in (let +TMP_41 \def (\lambda (c: C).(\lambda (w: T).(\lambda (u: T).(\lambda (_: (ty3 +g c w u)).(\lambda (H1: ((\forall (c2: C).((wf3 g c c2) \to (ty3 g c2 w +u))))).(\lambda (v: T).(\lambda (t: T).(\lambda (_: (ty3 g c v (THead (Bind +Abst) u t))).(\lambda (H3: ((\forall (c2: C).((wf3 g c c2) \to (ty3 g c2 v +(THead (Bind Abst) u t)))))).(\lambda (c2: C).(\lambda (H4: (wf3 g c +c2)).(let TMP_39 \def (H1 c2 H4) in (let TMP_40 \def (H3 c2 H4) in (ty3_appl +g c2 w u TMP_39 v t TMP_40)))))))))))))) in (let TMP_44 \def (\lambda (c: C).(\lambda (t3: T).(\lambda (t4: T).(\lambda (_: (ty3 g c t3 t4)).(\lambda (H1: ((\forall (c2: C).((wf3 g c c2) \to (ty3 g c2 t3 t4))))).(\lambda (t0: T).(\lambda (_: (ty3 g c t4 t0)).(\lambda (H3: ((\forall (c2: C).((wf3 g c c2) \to (ty3 g c2 t4 t0))))).(\lambda (c2: C).(\lambda (H4: (wf3 g c -c2)).(ty3_cast g c2 t3 t4 (H1 c2 H4) t0 (H3 c2 H4)))))))))))) c1 t1 t2 H))))). -(* COMMENTS -Initial nodes: 1027 -END *) +c2)).(let TMP_42 \def (H1 c2 H4) in (let TMP_43 \def (H3 c2 H4) in (ty3_cast +g c2 t3 t4 TMP_42 t0 TMP_43))))))))))))) in (ty3_ind g TMP_1 TMP_9 TMP_10 +TMP_21 TMP_32 TMP_38 TMP_41 TMP_44 c1 t1 t2 H))))))))))))). diff --git a/matita/matita/contribs/lambdadelta/basic_2/basic_1.txt b/matita/matita/contribs/lambdadelta/basic_2/basic_1.txt index 817f67b9c..0ff386374 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/basic_1.txt +++ b/matita/matita/contribs/lambdadelta/basic_2/basic_1.txt @@ -1,3 +1,12 @@ +# new ######################################################################## + +s_le_gen s_lt_gen +r_arith2 r_arith3 r_arith4 r_arith5 r_arith6 r_arith7 +tle tle_r +cle_r cle_head cle_trans_head cle_flt_trans +lift_tle lift_free_sym +subst0_gen_lift_rev_ge + # waiting #################################################################### aplus/props aplus_reg_r @@ -240,3 +249,4 @@ wf3/ty3 wf3_pc3_conf wf3/ty3 wf3_ty3_conf # check ###################################################################### +