1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 (* This file was automatically generated: do not edit *********************)
17 set "baseuri" "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/csubst1/fwd".
19 include "csubst1/defs.ma".
21 include "csubst0/fwd.ma".
23 include "subst1/props.ma".
25 theorem csubst1_gen_head:
26 \forall (k: K).(\forall (c1: C).(\forall (x: C).(\forall (u1: T).(\forall
27 (v: T).(\forall (i: nat).((csubst1 (s k i) v (CHead c1 k u1) x) \to (ex3_2 T
28 C (\lambda (u2: T).(\lambda (c2: C).(eq C x (CHead c2 k u2)))) (\lambda (u2:
29 T).(\lambda (_: C).(subst1 i v u1 u2))) (\lambda (_: T).(\lambda (c2:
30 C).(csubst1 i v c1 c2))))))))))
32 \lambda (k: K).(\lambda (c1: C).(\lambda (x: C).(\lambda (u1: T).(\lambda
33 (v: T).(\lambda (i: nat).(\lambda (H: (csubst1 (s k i) v (CHead c1 k u1)
34 x)).(let H0 \def (match H in csubst1 return (\lambda (c: C).(\lambda (_:
35 (csubst1 ? ? ? c)).((eq C c x) \to (ex3_2 T C (\lambda (u2: T).(\lambda (c2:
36 C).(eq C x (CHead c2 k u2)))) (\lambda (u2: T).(\lambda (_: C).(subst1 i v u1
37 u2))) (\lambda (_: T).(\lambda (c2: C).(csubst1 i v c1 c2))))))) with
38 [csubst1_refl \Rightarrow (\lambda (H0: (eq C (CHead c1 k u1) x)).(eq_ind C
39 (CHead c1 k u1) (\lambda (c: C).(ex3_2 T C (\lambda (u2: T).(\lambda (c2:
40 C).(eq C c (CHead c2 k u2)))) (\lambda (u2: T).(\lambda (_: C).(subst1 i v u1
41 u2))) (\lambda (_: T).(\lambda (c2: C).(csubst1 i v c1 c2))))) (ex3_2_intro T
42 C (\lambda (u2: T).(\lambda (c2: C).(eq C (CHead c1 k u1) (CHead c2 k u2))))
43 (\lambda (u2: T).(\lambda (_: C).(subst1 i v u1 u2))) (\lambda (_:
44 T).(\lambda (c2: C).(csubst1 i v c1 c2))) u1 c1 (refl_equal C (CHead c1 k
45 u1)) (subst1_refl i v u1) (csubst1_refl i v c1)) x H0)) | (csubst1_sing c2
46 H0) \Rightarrow (\lambda (H1: (eq C c2 x)).(eq_ind C x (\lambda (c:
47 C).((csubst0 (s k i) v (CHead c1 k u1) c) \to (ex3_2 T C (\lambda (u2:
48 T).(\lambda (c3: C).(eq C x (CHead c3 k u2)))) (\lambda (u2: T).(\lambda (_:
49 C).(subst1 i v u1 u2))) (\lambda (_: T).(\lambda (c3: C).(csubst1 i v c1
50 c3)))))) (\lambda (H2: (csubst0 (s k i) v (CHead c1 k u1) x)).(or3_ind (ex3_2
51 T nat (\lambda (_: T).(\lambda (j: nat).(eq nat (s k i) (s k j)))) (\lambda
52 (u2: T).(\lambda (_: nat).(eq C x (CHead c1 k u2)))) (\lambda (u2:
53 T).(\lambda (j: nat).(subst0 j v u1 u2)))) (ex3_2 C nat (\lambda (_:
54 C).(\lambda (j: nat).(eq nat (s k i) (s k j)))) (\lambda (c3: C).(\lambda (_:
55 nat).(eq C x (CHead c3 k u1)))) (\lambda (c3: C).(\lambda (j: nat).(csubst0 j
56 v c1 c3)))) (ex4_3 T C nat (\lambda (_: T).(\lambda (_: C).(\lambda (j:
57 nat).(eq nat (s k i) (s k j))))) (\lambda (u2: T).(\lambda (c3: C).(\lambda
58 (_: nat).(eq C x (CHead c3 k u2))))) (\lambda (u2: T).(\lambda (_:
59 C).(\lambda (j: nat).(subst0 j v u1 u2)))) (\lambda (_: T).(\lambda (c3:
60 C).(\lambda (j: nat).(csubst0 j v c1 c3))))) (ex3_2 T C (\lambda (u2:
61 T).(\lambda (c3: C).(eq C x (CHead c3 k u2)))) (\lambda (u2: T).(\lambda (_:
62 C).(subst1 i v u1 u2))) (\lambda (_: T).(\lambda (c3: C).(csubst1 i v c1
63 c3)))) (\lambda (H3: (ex3_2 T nat (\lambda (_: T).(\lambda (j: nat).(eq nat
64 (s k i) (s k j)))) (\lambda (u2: T).(\lambda (_: nat).(eq C x (CHead c1 k
65 u2)))) (\lambda (u2: T).(\lambda (j: nat).(subst0 j v u1 u2))))).(ex3_2_ind T
66 nat (\lambda (_: T).(\lambda (j: nat).(eq nat (s k i) (s k j)))) (\lambda
67 (u2: T).(\lambda (_: nat).(eq C x (CHead c1 k u2)))) (\lambda (u2:
68 T).(\lambda (j: nat).(subst0 j v u1 u2))) (ex3_2 T C (\lambda (u2:
69 T).(\lambda (c3: C).(eq C x (CHead c3 k u2)))) (\lambda (u2: T).(\lambda (_:
70 C).(subst1 i v u1 u2))) (\lambda (_: T).(\lambda (c3: C).(csubst1 i v c1
71 c3)))) (\lambda (x0: T).(\lambda (x1: nat).(\lambda (H: (eq nat (s k i) (s k
72 x1))).(\lambda (H4: (eq C x (CHead c1 k x0))).(\lambda (H5: (subst0 x1 v u1
73 x0)).(eq_ind_r C (CHead c1 k x0) (\lambda (c: C).(ex3_2 T C (\lambda (u2:
74 T).(\lambda (c3: C).(eq C c (CHead c3 k u2)))) (\lambda (u2: T).(\lambda (_:
75 C).(subst1 i v u1 u2))) (\lambda (_: T).(\lambda (c3: C).(csubst1 i v c1
76 c3))))) (let H6 \def (eq_ind_r nat x1 (\lambda (n: nat).(subst0 n v u1 x0))
77 H5 i (s_inj k i x1 H)) in (ex3_2_intro T C (\lambda (u2: T).(\lambda (c3:
78 C).(eq C (CHead c1 k x0) (CHead c3 k u2)))) (\lambda (u2: T).(\lambda (_:
79 C).(subst1 i v u1 u2))) (\lambda (_: T).(\lambda (c3: C).(csubst1 i v c1
80 c3))) x0 c1 (refl_equal C (CHead c1 k x0)) (subst1_single i v u1 x0 H6)
81 (csubst1_refl i v c1))) x H4)))))) H3)) (\lambda (H3: (ex3_2 C nat (\lambda
82 (_: C).(\lambda (j: nat).(eq nat (s k i) (s k j)))) (\lambda (c2: C).(\lambda
83 (_: nat).(eq C x (CHead c2 k u1)))) (\lambda (c2: C).(\lambda (j:
84 nat).(csubst0 j v c1 c2))))).(ex3_2_ind C nat (\lambda (_: C).(\lambda (j:
85 nat).(eq nat (s k i) (s k j)))) (\lambda (c3: C).(\lambda (_: nat).(eq C x
86 (CHead c3 k u1)))) (\lambda (c3: C).(\lambda (j: nat).(csubst0 j v c1 c3)))
87 (ex3_2 T C (\lambda (u2: T).(\lambda (c3: C).(eq C x (CHead c3 k u2))))
88 (\lambda (u2: T).(\lambda (_: C).(subst1 i v u1 u2))) (\lambda (_:
89 T).(\lambda (c3: C).(csubst1 i v c1 c3)))) (\lambda (x0: C).(\lambda (x1:
90 nat).(\lambda (H: (eq nat (s k i) (s k x1))).(\lambda (H4: (eq C x (CHead x0
91 k u1))).(\lambda (H5: (csubst0 x1 v c1 x0)).(eq_ind_r C (CHead x0 k u1)
92 (\lambda (c: C).(ex3_2 T C (\lambda (u2: T).(\lambda (c3: C).(eq C c (CHead
93 c3 k u2)))) (\lambda (u2: T).(\lambda (_: C).(subst1 i v u1 u2))) (\lambda
94 (_: T).(\lambda (c3: C).(csubst1 i v c1 c3))))) (let H6 \def (eq_ind_r nat x1
95 (\lambda (n: nat).(csubst0 n v c1 x0)) H5 i (s_inj k i x1 H)) in (ex3_2_intro
96 T C (\lambda (u2: T).(\lambda (c3: C).(eq C (CHead x0 k u1) (CHead c3 k
97 u2)))) (\lambda (u2: T).(\lambda (_: C).(subst1 i v u1 u2))) (\lambda (_:
98 T).(\lambda (c3: C).(csubst1 i v c1 c3))) u1 x0 (refl_equal C (CHead x0 k
99 u1)) (subst1_refl i v u1) (csubst1_sing i v c1 x0 H6))) x H4)))))) H3))
100 (\lambda (H3: (ex4_3 T C nat (\lambda (_: T).(\lambda (_: C).(\lambda (j:
101 nat).(eq nat (s k i) (s k j))))) (\lambda (u2: T).(\lambda (c2: C).(\lambda
102 (_: nat).(eq C x (CHead c2 k u2))))) (\lambda (u2: T).(\lambda (_:
103 C).(\lambda (j: nat).(subst0 j v u1 u2)))) (\lambda (_: T).(\lambda (c2:
104 C).(\lambda (j: nat).(csubst0 j v c1 c2)))))).(ex4_3_ind T C nat (\lambda (_:
105 T).(\lambda (_: C).(\lambda (j: nat).(eq nat (s k i) (s k j))))) (\lambda
106 (u2: T).(\lambda (c3: C).(\lambda (_: nat).(eq C x (CHead c3 k u2)))))
107 (\lambda (u2: T).(\lambda (_: C).(\lambda (j: nat).(subst0 j v u1 u2))))
108 (\lambda (_: T).(\lambda (c3: C).(\lambda (j: nat).(csubst0 j v c1 c3))))
109 (ex3_2 T C (\lambda (u2: T).(\lambda (c3: C).(eq C x (CHead c3 k u2))))
110 (\lambda (u2: T).(\lambda (_: C).(subst1 i v u1 u2))) (\lambda (_:
111 T).(\lambda (c3: C).(csubst1 i v c1 c3)))) (\lambda (x0: T).(\lambda (x1:
112 C).(\lambda (x2: nat).(\lambda (H: (eq nat (s k i) (s k x2))).(\lambda (H4:
113 (eq C x (CHead x1 k x0))).(\lambda (H5: (subst0 x2 v u1 x0)).(\lambda (H6:
114 (csubst0 x2 v c1 x1)).(eq_ind_r C (CHead x1 k x0) (\lambda (c: C).(ex3_2 T C
115 (\lambda (u2: T).(\lambda (c3: C).(eq C c (CHead c3 k u2)))) (\lambda (u2:
116 T).(\lambda (_: C).(subst1 i v u1 u2))) (\lambda (_: T).(\lambda (c3:
117 C).(csubst1 i v c1 c3))))) (let H7 \def (eq_ind_r nat x2 (\lambda (n:
118 nat).(csubst0 n v c1 x1)) H6 i (s_inj k i x2 H)) in (let H8 \def (eq_ind_r
119 nat x2 (\lambda (n: nat).(subst0 n v u1 x0)) H5 i (s_inj k i x2 H)) in
120 (ex3_2_intro T C (\lambda (u2: T).(\lambda (c3: C).(eq C (CHead x1 k x0)
121 (CHead c3 k u2)))) (\lambda (u2: T).(\lambda (_: C).(subst1 i v u1 u2)))
122 (\lambda (_: T).(\lambda (c3: C).(csubst1 i v c1 c3))) x0 x1 (refl_equal C
123 (CHead x1 k x0)) (subst1_single i v u1 x0 H8) (csubst1_sing i v c1 x1 H7))))
124 x H4)))))))) H3)) (csubst0_gen_head k c1 x u1 v (s k i) H2))) c2 (sym_eq C c2
125 x H1) H0))]) in (H0 (refl_equal C x))))))))).