matita/matita/contribs/lambdadelta/basic_1/wcpr0/fwd.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 (* This file was automatically generated: do not edit *********************)
  16
  17 include "basic_1/wcpr0/defs.ma".
  18
  19 let rec wcpr0_ind (P: (C \to (C \to Prop))) (f: (\forall (c: C).(P c c)))
  20 (f0: (\forall (c1: C).(\forall (c2: C).((wcpr0 c1 c2) \to ((P c1 c2) \to
  21 (\forall (u1: T).(\forall (u2: T).((pr0 u1 u2) \to (\forall (k: K).(P (CHead
  22 c1 k u1) (CHead c2 k u2))))))))))) (c: C) (c0: C) (w: wcpr0 c c0) on w: P c
  23 c0 \def match w with [(wcpr0_refl c1) \Rightarrow (f c1) | (wcpr0_comp c1 c2
  24 w0 u1 u2 p k) \Rightarrow (let TMP_1 \def ((wcpr0_ind P f f0) c1 c2 w0) in
  25 (f0 c1 c2 w0 TMP_1 u1 u2 p k))].
  26
  27 theorem wcpr0_gen_sort:
  28  \forall (x: C).(\forall (n: nat).((wcpr0 (CSort n) x) \to (eq C x (CSort
  29 n))))
  30 \def
  31  \lambda (x: C).(\lambda (n: nat).(\lambda (H: (wcpr0 (CSort n) x)).(let
  32 TMP_1 \def (CSort n) in (let TMP_2 \def (\lambda (c: C).(wcpr0 c x)) in (let
  33 TMP_3 \def (\lambda (c: C).(eq C x c)) in (let TMP_19 \def (\lambda (y:
  34 C).(\lambda (H0: (wcpr0 y x)).(let TMP_4 \def (\lambda (c: C).(\lambda (c0:
  35 C).((eq C c (CSort n)) \to (eq C c0 c)))) in (let TMP_11 \def (\lambda (c:
  36 C).(\lambda (H1: (eq C c (CSort n))).(let TMP_5 \def (\lambda (e: C).e) in
  37 (let TMP_6 \def (CSort n) in (let H2 \def (f_equal C C TMP_5 c TMP_6 H1) in
  38 (let TMP_7 \def (CSort n) in (let TMP_8 \def (\lambda (c0: C).(eq C c0 c0))
  39 in (let TMP_9 \def (CSort n) in (let TMP_10 \def (refl_equal C TMP_9) in
  40 (eq_ind_r C TMP_7 TMP_8 TMP_10 c H2)))))))))) in (let TMP_18 \def (\lambda
  41 (c1: C).(\lambda (c2: C).(\lambda (_: (wcpr0 c1 c2)).(\lambda (_: (((eq C c1
  42 (CSort n)) \to (eq C c2 c1)))).(\lambda (u1: T).(\lambda (u2: T).(\lambda (_:
  43 (pr0 u1 u2)).(\lambda (k: K).(\lambda (H4: (eq C (CHead c1 k u1) (CSort
  44 n))).(let TMP_12 \def (CHead c1 k u1) in (let TMP_13 \def (\lambda (ee:
  45 C).(match ee with [(CSort _) \Rightarrow False | (CHead _ _ _) \Rightarrow
  46 True])) in (let TMP_14 \def (CSort n) in (let H5 \def (eq_ind C TMP_12 TMP_13
  47 I TMP_14 H4) in (let TMP_15 \def (CHead c2 k u2) in (let TMP_16 \def (CHead
  48 c1 k u1) in (let TMP_17 \def (eq C TMP_15 TMP_16) in (False_ind TMP_17
  49 H5))))))))))))))))) in (wcpr0_ind TMP_4 TMP_11 TMP_18 y x H0)))))) in
  50 (insert_eq C TMP_1 TMP_2 TMP_3 TMP_19 H))))))).
  51
  52 theorem wcpr0_gen_head:
  53  \forall (k: K).(\forall (c1: C).(\forall (x: C).(\forall (u1: T).((wcpr0
  54 (CHead c1 k u1) x) \to (or (eq C x (CHead c1 k u1)) (ex3_2 C T (\lambda (c2:
  55 C).(\lambda (u2: T).(eq C x (CHead c2 k u2)))) (\lambda (c2: C).(\lambda (_:
  56 T).(wcpr0 c1 c2))) (\lambda (_: C).(\lambda (u2: T).(pr0 u1 u2)))))))))
  57 \def
  58  \lambda (k: K).(\lambda (c1: C).(\lambda (x: C).(\lambda (u1: T).(\lambda
  59 (H: (wcpr0 (CHead c1 k u1) x)).(let TMP_1 \def (CHead c1 k u1) in (let TMP_2
  60 \def (\lambda (c: C).(wcpr0 c x)) in (let TMP_9 \def (\lambda (c: C).(let
  61 TMP_3 \def (eq C x c) in (let TMP_5 \def (\lambda (c2: C).(\lambda (u2:
  62 T).(let TMP_4 \def (CHead c2 k u2) in (eq C x TMP_4)))) in (let TMP_6 \def
  63 (\lambda (c2: C).(\lambda (_: T).(wcpr0 c1 c2))) in (let TMP_7 \def (\lambda
  64 (_: C).(\lambda (u2: T).(pr0 u1 u2))) in (let TMP_8 \def (ex3_2 C T TMP_5
  65 TMP_6 TMP_7) in (or TMP_3 TMP_8))))))) in (let TMP_111 \def (\lambda (y:
  66 C).(\lambda (H0: (wcpr0 y x)).(let TMP_16 \def (\lambda (c: C).(\lambda (c0:
  67 C).((eq C c (CHead c1 k u1)) \to (let TMP_10 \def (eq C c0 c) in (let TMP_12
  68 \def (\lambda (c2: C).(\lambda (u2: T).(let TMP_11 \def (CHead c2 k u2) in
  69 (eq C c0 TMP_11)))) in (let TMP_13 \def (\lambda (c2: C).(\lambda (_:
  70 T).(wcpr0 c1 c2))) in (let TMP_14 \def (\lambda (_: C).(\lambda (u2: T).(pr0
  71 u1 u2))) in (let TMP_15 \def (ex3_2 C T TMP_12 TMP_13 TMP_14) in (or TMP_10
  72 TMP_15))))))))) in (let TMP_39 \def (\lambda (c: C).(\lambda (H1: (eq C c
  73 (CHead c1 k u1))).(let TMP_17 \def (\lambda (e: C).e) in (let TMP_18 \def
  74 (CHead c1 k u1) in (let H2 \def (f_equal C C TMP_17 c TMP_18 H1) in (let
  75 TMP_19 \def (CHead c1 k u1) in (let TMP_26 \def (\lambda (c0: C).(let TMP_20
  76 \def (eq C c0 c0) in (let TMP_22 \def (\lambda (c2: C).(\lambda (u2: T).(let
  77 TMP_21 \def (CHead c2 k u2) in (eq C c0 TMP_21)))) in (let TMP_23 \def
  78 (\lambda (c2: C).(\lambda (_: T).(wcpr0 c1 c2))) in (let TMP_24 \def (\lambda
  79 (_: C).(\lambda (u2: T).(pr0 u1 u2))) in (let TMP_25 \def (ex3_2 C T TMP_22
  80 TMP_23 TMP_24) in (or TMP_20 TMP_25))))))) in (let TMP_27 \def (CHead c1 k
  81 u1) in (let TMP_28 \def (CHead c1 k u1) in (let TMP_29 \def (eq C TMP_27
  82 TMP_28) in (let TMP_32 \def (\lambda (c2: C).(\lambda (u2: T).(let TMP_30
  83 \def (CHead c1 k u1) in (let TMP_31 \def (CHead c2 k u2) in (eq C TMP_30
  84 TMP_31))))) in (let TMP_33 \def (\lambda (c2: C).(\lambda (_: T).(wcpr0 c1
  85 c2))) in (let TMP_34 \def (\lambda (_: C).(\lambda (u2: T).(pr0 u1 u2))) in
  86 (let TMP_35 \def (ex3_2 C T TMP_32 TMP_33 TMP_34) in (let TMP_36 \def (CHead
  87 c1 k u1) in (let TMP_37 \def (refl_equal C TMP_36) in (let TMP_38 \def
  88 (or_introl TMP_29 TMP_35 TMP_37) in (eq_ind_r C TMP_19 TMP_26 TMP_38 c
  89 H2)))))))))))))))))) in (let TMP_110 \def (\lambda (c0: C).(\lambda (c2:
  90 C).(\lambda (H1: (wcpr0 c0 c2)).(\lambda (H2: (((eq C c0 (CHead c1 k u1)) \to
  91 (or (eq C c2 c0) (ex3_2 C T (\lambda (c3: C).(\lambda (u2: T).(eq C c2 (CHead
  92 c3 k u2)))) (\lambda (c3: C).(\lambda (_: T).(wcpr0 c1 c3))) (\lambda (_:
  93 C).(\lambda (u2: T).(pr0 u1 u2)))))))).(\lambda (u0: T).(\lambda (u2:
  94 T).(\lambda (H3: (pr0 u0 u2)).(\lambda (k0: K).(\lambda (H4: (eq C (CHead c0
  95 k0 u0) (CHead c1 k u1))).(let TMP_40 \def (\lambda (e: C).(match e with
  96 [(CSort _) \Rightarrow c0 | (CHead c _ _) \Rightarrow c])) in (let TMP_41
  97 \def (CHead c0 k0 u0) in (let TMP_42 \def (CHead c1 k u1) in (let H5 \def
  98 (f_equal C C TMP_40 TMP_41 TMP_42 H4) in (let TMP_43 \def (\lambda (e:
  99 C).(match e with [(CSort _) \Rightarrow k0 | (CHead _ k1 _) \Rightarrow k1]))
 100 in (let TMP_44 \def (CHead c0 k0 u0) in (let TMP_45 \def (CHead c1 k u1) in
 101 (let H6 \def (f_equal C K TMP_43 TMP_44 TMP_45 H4) in (let TMP_46 \def
 102 (\lambda (e: C).(match e with [(CSort _) \Rightarrow u0 | (CHead _ _ t)
 103 \Rightarrow t])) in (let TMP_47 \def (CHead c0 k0 u0) in (let TMP_48 \def
 104 (CHead c1 k u1) in (let H7 \def (f_equal C T TMP_46 TMP_47 TMP_48 H4) in (let
 105 TMP_108 \def (\lambda (H8: (eq K k0 k)).(\lambda (H9: (eq C c0 c1)).(let
 106 TMP_58 \def (\lambda (k1: K).(let TMP_49 \def (CHead c2 k1 u2) in (let TMP_50
 107 \def (CHead c0 k1 u0) in (let TMP_51 \def (eq C TMP_49 TMP_50) in (let TMP_54
 108 \def (\lambda (c3: C).(\lambda (u3: T).(let TMP_52 \def (CHead c2 k1 u2) in
 109 (let TMP_53 \def (CHead c3 k u3) in (eq C TMP_52 TMP_53))))) in (let TMP_55
 110 \def (\lambda (c3: C).(\lambda (_: T).(wcpr0 c1 c3))) in (let TMP_56 \def
 111 (\lambda (_: C).(\lambda (u3: T).(pr0 u1 u3))) in (let TMP_57 \def (ex3_2 C T
 112 TMP_54 TMP_55 TMP_56) in (or TMP_51 TMP_57))))))))) in (let TMP_59 \def
 113 (\lambda (t: T).(pr0 t u2)) in (let H10 \def (eq_ind T u0 TMP_59 H3 u1 H7) in
 114 (let TMP_69 \def (\lambda (t: T).(let TMP_60 \def (CHead c2 k u2) in (let
 115 TMP_61 \def (CHead c0 k t) in (let TMP_62 \def (eq C TMP_60 TMP_61) in (let
 116 TMP_65 \def (\lambda (c3: C).(\lambda (u3: T).(let TMP_63 \def (CHead c2 k
 117 u2) in (let TMP_64 \def (CHead c3 k u3) in (eq C TMP_63 TMP_64))))) in (let
 118 TMP_66 \def (\lambda (c3: C).(\lambda (_: T).(wcpr0 c1 c3))) in (let TMP_67
 119 \def (\lambda (_: C).(\lambda (u3: T).(pr0 u1 u3))) in (let TMP_68 \def
 120 (ex3_2 C T TMP_65 TMP_66 TMP_67) in (or TMP_62 TMP_68))))))))) in (let TMP_76
 121 \def (\lambda (c: C).((eq C c (CHead c1 k u1)) \to (let TMP_70 \def (eq C c2
 122 c) in (let TMP_72 \def (\lambda (c3: C).(\lambda (u3: T).(let TMP_71 \def
 123 (CHead c3 k u3) in (eq C c2 TMP_71)))) in (let TMP_73 \def (\lambda (c3:
 124 C).(\lambda (_: T).(wcpr0 c1 c3))) in (let TMP_74 \def (\lambda (_:
 125 C).(\lambda (u3: T).(pr0 u1 u3))) in (let TMP_75 \def (ex3_2 C T TMP_72
 126 TMP_73 TMP_74) in (or TMP_70 TMP_75)))))))) in (let H11 \def (eq_ind C c0
 127 TMP_76 H2 c1 H9) in (let TMP_77 \def (\lambda (c: C).(wcpr0 c c2)) in (let
 128 H12 \def (eq_ind C c0 TMP_77 H1 c1 H9) in (let TMP_87 \def (\lambda (c:
 129 C).(let TMP_78 \def (CHead c2 k u2) in (let TMP_79 \def (CHead c k u1) in
 130 (let TMP_80 \def (eq C TMP_78 TMP_79) in (let TMP_83 \def (\lambda (c3:
 131 C).(\lambda (u3: T).(let TMP_81 \def (CHead c2 k u2) in (let TMP_82 \def
 132 (CHead c3 k u3) in (eq C TMP_81 TMP_82))))) in (let TMP_84 \def (\lambda (c3:
 133 C).(\lambda (_: T).(wcpr0 c1 c3))) in (let TMP_85 \def (\lambda (_:
 134 C).(\lambda (u3: T).(pr0 u1 u3))) in (let TMP_86 \def (ex3_2 C T TMP_83
 135 TMP_84 TMP_85) in (or TMP_80 TMP_86))))))))) in (let TMP_88 \def (CHead c2 k
 136 u2) in (let TMP_89 \def (CHead c1 k u1) in (let TMP_90 \def (eq C TMP_88
 137 TMP_89) in (let TMP_93 \def (\lambda (c3: C).(\lambda (u3: T).(let TMP_91
 138 \def (CHead c2 k u2) in (let TMP_92 \def (CHead c3 k u3) in (eq C TMP_91
 139 TMP_92))))) in (let TMP_94 \def (\lambda (c3: C).(\lambda (_: T).(wcpr0 c1
 140 c3))) in (let TMP_95 \def (\lambda (_: C).(\lambda (u3: T).(pr0 u1 u3))) in
 141 (let TMP_96 \def (ex3_2 C T TMP_93 TMP_94 TMP_95) in (let TMP_99 \def
 142 (\lambda (c3: C).(\lambda (u3: T).(let TMP_97 \def (CHead c2 k u2) in (let
 143 TMP_98 \def (CHead c3 k u3) in (eq C TMP_97 TMP_98))))) in (let TMP_100 \def
 144 (\lambda (c3: C).(\lambda (_: T).(wcpr0 c1 c3))) in (let TMP_101 \def
 145 (\lambda (_: C).(\lambda (u3: T).(pr0 u1 u3))) in (let TMP_102 \def (CHead c2
 146 k u2) in (let TMP_103 \def (refl_equal C TMP_102) in (let TMP_104 \def
 147 (ex3_2_intro C T TMP_99 TMP_100 TMP_101 c2 u2 TMP_103 H12 H10) in (let
 148 TMP_105 \def (or_intror TMP_90 TMP_96 TMP_104) in (let TMP_106 \def (eq_ind_r
 149 C c1 TMP_87 TMP_105 c0 H9) in (let TMP_107 \def (eq_ind_r T u1 TMP_69 TMP_106
 150 u0 H7) in (eq_ind_r K k TMP_58 TMP_107 k0 H8)))))))))))))))))))))))))))) in
 151 (let TMP_109 \def (TMP_108 H6) in (TMP_109 H5)))))))))))))))))))))))) in
 152 (wcpr0_ind TMP_16 TMP_39 TMP_110 y x H0)))))) in (insert_eq C TMP_1 TMP_2
 153 TMP_9 TMP_111 H))))))))).
 154