helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubst1/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 "csubst1/defs.ma".
  18
  19 include "csubst0/fwd.ma".
  20
  21 include "subst1/props.ma".
  22
  23 theorem csubst1_gen_head:
  24  \forall (k: K).(\forall (c1: C).(\forall (x: C).(\forall (u1: T).(\forall
  25 (v: T).(\forall (i: nat).((csubst1 (s k i) v (CHead c1 k u1) x) \to (ex3_2 T
  26 C (\lambda (u2: T).(\lambda (c2: C).(eq C x (CHead c2 k u2)))) (\lambda (u2:
  27 T).(\lambda (_: C).(subst1 i v u1 u2))) (\lambda (_: T).(\lambda (c2:
  28 C).(csubst1 i v c1 c2))))))))))
  29 \def
  30  \lambda (k: K).(\lambda (c1: C).(\lambda (x: C).(\lambda (u1: T).(\lambda
  31 (v: T).(\lambda (i: nat).(\lambda (H: (csubst1 (s k i) v (CHead c1 k u1)
  32 x)).(let H0 \def (match H in csubst1 return (\lambda (c: C).(\lambda (_:
  33 (csubst1 ? ? ? c)).((eq C c x) \to (ex3_2 T C (\lambda (u2: T).(\lambda (c2:
  34 C).(eq C x (CHead c2 k u2)))) (\lambda (u2: T).(\lambda (_: C).(subst1 i v u1
  35 u2))) (\lambda (_: T).(\lambda (c2: C).(csubst1 i v c1 c2))))))) with
  36 [csubst1_refl \Rightarrow (\lambda (H0: (eq C (CHead c1 k u1) x)).(eq_ind C
  37 (CHead c1 k u1) (\lambda (c: C).(ex3_2 T C (\lambda (u2: T).(\lambda (c2:
  38 C).(eq C c (CHead c2 k u2)))) (\lambda (u2: T).(\lambda (_: C).(subst1 i v u1
  39 u2))) (\lambda (_: T).(\lambda (c2: C).(csubst1 i v c1 c2))))) (ex3_2_intro T
  40 C (\lambda (u2: T).(\lambda (c2: C).(eq C (CHead c1 k u1) (CHead c2 k u2))))
  41 (\lambda (u2: T).(\lambda (_: C).(subst1 i v u1 u2))) (\lambda (_:
  42 T).(\lambda (c2: C).(csubst1 i v c1 c2))) u1 c1 (refl_equal C (CHead c1 k
  43 u1)) (subst1_refl i v u1) (csubst1_refl i v c1)) x H0)) | (csubst1_sing c2
  44 H0) \Rightarrow (\lambda (H1: (eq C c2 x)).(eq_ind C x (\lambda (c:
  45 C).((csubst0 (s k i) v (CHead c1 k u1) c) \to (ex3_2 T C (\lambda (u2:
  46 T).(\lambda (c3: C).(eq C x (CHead c3 k u2)))) (\lambda (u2: T).(\lambda (_:
  47 C).(subst1 i v u1 u2))) (\lambda (_: T).(\lambda (c3: C).(csubst1 i v c1
  48 c3)))))) (\lambda (H2: (csubst0 (s k i) v (CHead c1 k u1) x)).(or3_ind (ex3_2
  49 T nat (\lambda (_: T).(\lambda (j: nat).(eq nat (s k i) (s k j)))) (\lambda
  50 (u2: T).(\lambda (_: nat).(eq C x (CHead c1 k u2)))) (\lambda (u2:
  51 T).(\lambda (j: nat).(subst0 j v u1 u2)))) (ex3_2 C nat (\lambda (_:
  52 C).(\lambda (j: nat).(eq nat (s k i) (s k j)))) (\lambda (c3: C).(\lambda (_:
  53 nat).(eq C x (CHead c3 k u1)))) (\lambda (c3: C).(\lambda (j: nat).(csubst0 j
  54 v c1 c3)))) (ex4_3 T C nat (\lambda (_: T).(\lambda (_: C).(\lambda (j:
  55 nat).(eq nat (s k i) (s k j))))) (\lambda (u2: T).(\lambda (c3: C).(\lambda
  56 (_: nat).(eq C x (CHead c3 k u2))))) (\lambda (u2: T).(\lambda (_:
  57 C).(\lambda (j: nat).(subst0 j v u1 u2)))) (\lambda (_: T).(\lambda (c3:
  58 C).(\lambda (j: nat).(csubst0 j v c1 c3))))) (ex3_2 T C (\lambda (u2:
  59 T).(\lambda (c3: C).(eq C x (CHead c3 k u2)))) (\lambda (u2: T).(\lambda (_:
  60 C).(subst1 i v u1 u2))) (\lambda (_: T).(\lambda (c3: C).(csubst1 i v c1
  61 c3)))) (\lambda (H3: (ex3_2 T nat (\lambda (_: T).(\lambda (j: nat).(eq nat
  62 (s k i) (s k j)))) (\lambda (u2: T).(\lambda (_: nat).(eq C x (CHead c1 k
  63 u2)))) (\lambda (u2: T).(\lambda (j: nat).(subst0 j v u1 u2))))).(ex3_2_ind T
  64 nat (\lambda (_: T).(\lambda (j: nat).(eq nat (s k i) (s k j)))) (\lambda
  65 (u2: T).(\lambda (_: nat).(eq C x (CHead c1 k u2)))) (\lambda (u2:
  66 T).(\lambda (j: nat).(subst0 j v u1 u2))) (ex3_2 T C (\lambda (u2:
  67 T).(\lambda (c3: C).(eq C x (CHead c3 k u2)))) (\lambda (u2: T).(\lambda (_:
  68 C).(subst1 i v u1 u2))) (\lambda (_: T).(\lambda (c3: C).(csubst1 i v c1
  69 c3)))) (\lambda (x0: T).(\lambda (x1: nat).(\lambda (H4: (eq nat (s k i) (s k
  70 x1))).(\lambda (H5: (eq C x (CHead c1 k x0))).(\lambda (H6: (subst0 x1 v u1
  71 x0)).(eq_ind_r C (CHead c1 k x0) (\lambda (c: C).(ex3_2 T C (\lambda (u2:
  72 T).(\lambda (c3: C).(eq C c (CHead c3 k u2)))) (\lambda (u2: T).(\lambda (_:
  73 C).(subst1 i v u1 u2))) (\lambda (_: T).(\lambda (c3: C).(csubst1 i v c1
  74 c3))))) (let H7 \def (eq_ind_r nat x1 (\lambda (n: nat).(subst0 n v u1 x0))
  75 H6 i (s_inj k i x1 H4)) in (ex3_2_intro T C (\lambda (u2: T).(\lambda (c3:
  76 C).(eq C (CHead c1 k x0) (CHead c3 k u2)))) (\lambda (u2: T).(\lambda (_:
  77 C).(subst1 i v u1 u2))) (\lambda (_: T).(\lambda (c3: C).(csubst1 i v c1
  78 c3))) x0 c1 (refl_equal C (CHead c1 k x0)) (subst1_single i v u1 x0 H7)
  79 (csubst1_refl i v c1))) x H5)))))) H3)) (\lambda (H3: (ex3_2 C nat (\lambda
  80 (_: C).(\lambda (j: nat).(eq nat (s k i) (s k j)))) (\lambda (c3: C).(\lambda
  81 (_: nat).(eq C x (CHead c3 k u1)))) (\lambda (c3: C).(\lambda (j:
  82 nat).(csubst0 j v c1 c3))))).(ex3_2_ind C nat (\lambda (_: C).(\lambda (j:
  83 nat).(eq nat (s k i) (s k j)))) (\lambda (c3: C).(\lambda (_: nat).(eq C x
  84 (CHead c3 k u1)))) (\lambda (c3: C).(\lambda (j: nat).(csubst0 j v c1 c3)))
  85 (ex3_2 T C (\lambda (u2: T).(\lambda (c3: C).(eq C x (CHead c3 k u2))))
  86 (\lambda (u2: T).(\lambda (_: C).(subst1 i v u1 u2))) (\lambda (_:
  87 T).(\lambda (c3: C).(csubst1 i v c1 c3)))) (\lambda (x0: C).(\lambda (x1:
  88 nat).(\lambda (H4: (eq nat (s k i) (s k x1))).(\lambda (H5: (eq C x (CHead x0
  89 k u1))).(\lambda (H6: (csubst0 x1 v c1 x0)).(eq_ind_r C (CHead x0 k u1)
  90 (\lambda (c: C).(ex3_2 T C (\lambda (u2: T).(\lambda (c3: C).(eq C c (CHead
  91 c3 k u2)))) (\lambda (u2: T).(\lambda (_: C).(subst1 i v u1 u2))) (\lambda
  92 (_: T).(\lambda (c3: C).(csubst1 i v c1 c3))))) (let H7 \def (eq_ind_r nat x1
  93 (\lambda (n: nat).(csubst0 n v c1 x0)) H6 i (s_inj k i x1 H4)) in
  94 (ex3_2_intro T C (\lambda (u2: T).(\lambda (c3: C).(eq C (CHead x0 k u1)
  95 (CHead c3 k u2)))) (\lambda (u2: T).(\lambda (_: C).(subst1 i v u1 u2)))
  96 (\lambda (_: T).(\lambda (c3: C).(csubst1 i v c1 c3))) u1 x0 (refl_equal C
  97 (CHead x0 k u1)) (subst1_refl i v u1) (csubst1_sing i v c1 x0 H7))) x
  98 H5)))))) H3)) (\lambda (H3: (ex4_3 T C nat (\lambda (_: T).(\lambda (_:
  99 C).(\lambda (j: nat).(eq nat (s k i) (s k j))))) (\lambda (u2: T).(\lambda
 100 (c3: C).(\lambda (_: nat).(eq C x (CHead c3 k u2))))) (\lambda (u2:
 101 T).(\lambda (_: C).(\lambda (j: nat).(subst0 j v u1 u2)))) (\lambda (_:
 102 T).(\lambda (c3: C).(\lambda (j: nat).(csubst0 j v c1 c3)))))).(ex4_3_ind T C
 103 nat (\lambda (_: T).(\lambda (_: C).(\lambda (j: nat).(eq nat (s k i) (s k
 104 j))))) (\lambda (u2: T).(\lambda (c3: C).(\lambda (_: nat).(eq C x (CHead c3
 105 k u2))))) (\lambda (u2: T).(\lambda (_: C).(\lambda (j: nat).(subst0 j v u1
 106 u2)))) (\lambda (_: T).(\lambda (c3: C).(\lambda (j: nat).(csubst0 j v c1
 107 c3)))) (ex3_2 T C (\lambda (u2: T).(\lambda (c3: C).(eq C x (CHead c3 k
 108 u2)))) (\lambda (u2: T).(\lambda (_: C).(subst1 i v u1 u2))) (\lambda (_:
 109 T).(\lambda (c3: C).(csubst1 i v c1 c3)))) (\lambda (x0: T).(\lambda (x1:
 110 C).(\lambda (x2: nat).(\lambda (H4: (eq nat (s k i) (s k x2))).(\lambda (H5:
 111 (eq C x (CHead x1 k x0))).(\lambda (H6: (subst0 x2 v u1 x0)).(\lambda (H7:
 112 (csubst0 x2 v c1 x1)).(eq_ind_r C (CHead x1 k x0) (\lambda (c: C).(ex3_2 T C
 113 (\lambda (u2: T).(\lambda (c3: C).(eq C c (CHead c3 k u2)))) (\lambda (u2:
 114 T).(\lambda (_: C).(subst1 i v u1 u2))) (\lambda (_: T).(\lambda (c3:
 115 C).(csubst1 i v c1 c3))))) (let H8 \def (eq_ind_r nat x2 (\lambda (n:
 116 nat).(csubst0 n v c1 x1)) H7 i (s_inj k i x2 H4)) in (let H9 \def (eq_ind_r
 117 nat x2 (\lambda (n: nat).(subst0 n v u1 x0)) H6 i (s_inj k i x2 H4)) in
 118 (ex3_2_intro T C (\lambda (u2: T).(\lambda (c3: C).(eq C (CHead x1 k x0)
 119 (CHead c3 k u2)))) (\lambda (u2: T).(\lambda (_: C).(subst1 i v u1 u2)))
 120 (\lambda (_: T).(\lambda (c3: C).(csubst1 i v c1 c3))) x0 x1 (refl_equal C
 121 (CHead x1 k x0)) (subst1_single i v u1 x0 H9) (csubst1_sing i v c1 x1 H8))))
 122 x H5)))))))) H3)) (csubst0_gen_head k c1 x u1 v (s k i) H2))) c2 (sym_eq C c2
 123 x H1) H0))]) in (H0 (refl_equal C x))))))))).
 124