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 include "LambdaDelta-1/csubst1/defs.ma".
19 include "LambdaDelta-1/csubst0/fwd.ma".
21 include "LambdaDelta-1/subst1/props.ma".
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))))))))))
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)).(csubst1_ind (s k i) v (CHead c1 k u1) (\lambda (c: C).(ex3_2 T C
33 (\lambda (u2: T).(\lambda (c2: C).(eq C c (CHead c2 k u2)))) (\lambda (u2:
34 T).(\lambda (_: C).(subst1 i v u1 u2))) (\lambda (_: T).(\lambda (c2:
35 C).(csubst1 i v c1 c2))))) (ex3_2_intro T C (\lambda (u2: T).(\lambda (c2:
36 C).(eq C (CHead c1 k u1) (CHead c2 k u2)))) (\lambda (u2: T).(\lambda (_:
37 C).(subst1 i v u1 u2))) (\lambda (_: T).(\lambda (c2: C).(csubst1 i v c1
38 c2))) u1 c1 (refl_equal C (CHead c1 k u1)) (subst1_refl i v u1) (csubst1_refl
39 i v c1)) (\lambda (c2: C).(\lambda (H0: (csubst0 (s k i) v (CHead c1 k u1)
40 c2)).(or3_ind (ex3_2 T nat (\lambda (_: T).(\lambda (j: nat).(eq nat (s k i)
41 (s k j)))) (\lambda (u2: T).(\lambda (_: nat).(eq C c2 (CHead c1 k u2))))
42 (\lambda (u2: T).(\lambda (j: nat).(subst0 j v u1 u2)))) (ex3_2 C nat
43 (\lambda (_: C).(\lambda (j: nat).(eq nat (s k i) (s k j)))) (\lambda (c3:
44 C).(\lambda (_: nat).(eq C c2 (CHead c3 k u1)))) (\lambda (c3: C).(\lambda
45 (j: nat).(csubst0 j v c1 c3)))) (ex4_3 T C nat (\lambda (_: T).(\lambda (_:
46 C).(\lambda (j: nat).(eq nat (s k i) (s k j))))) (\lambda (u2: T).(\lambda
47 (c3: C).(\lambda (_: nat).(eq C c2 (CHead c3 k u2))))) (\lambda (u2:
48 T).(\lambda (_: C).(\lambda (j: nat).(subst0 j v u1 u2)))) (\lambda (_:
49 T).(\lambda (c3: C).(\lambda (j: nat).(csubst0 j v c1 c3))))) (ex3_2 T C
50 (\lambda (u2: T).(\lambda (c3: C).(eq C c2 (CHead c3 k u2)))) (\lambda (u2:
51 T).(\lambda (_: C).(subst1 i v u1 u2))) (\lambda (_: T).(\lambda (c3:
52 C).(csubst1 i v c1 c3)))) (\lambda (H1: (ex3_2 T nat (\lambda (_: T).(\lambda
53 (j: nat).(eq nat (s k i) (s k j)))) (\lambda (u2: T).(\lambda (_: nat).(eq C
54 c2 (CHead c1 k u2)))) (\lambda (u2: T).(\lambda (j: nat).(subst0 j v u1
55 u2))))).(ex3_2_ind T nat (\lambda (_: T).(\lambda (j: nat).(eq nat (s k i) (s
56 k j)))) (\lambda (u2: T).(\lambda (_: nat).(eq C c2 (CHead c1 k u2))))
57 (\lambda (u2: T).(\lambda (j: nat).(subst0 j v u1 u2))) (ex3_2 T C (\lambda
58 (u2: T).(\lambda (c3: C).(eq C c2 (CHead c3 k u2)))) (\lambda (u2:
59 T).(\lambda (_: C).(subst1 i v u1 u2))) (\lambda (_: T).(\lambda (c3:
60 C).(csubst1 i v c1 c3)))) (\lambda (x0: T).(\lambda (x1: nat).(\lambda (H2:
61 (eq nat (s k i) (s k x1))).(\lambda (H3: (eq C c2 (CHead c1 k x0))).(\lambda
62 (H4: (subst0 x1 v u1 x0)).(eq_ind_r C (CHead c1 k x0) (\lambda (c: C).(ex3_2
63 T C (\lambda (u2: T).(\lambda (c3: C).(eq C c (CHead c3 k u2)))) (\lambda
64 (u2: T).(\lambda (_: C).(subst1 i v u1 u2))) (\lambda (_: T).(\lambda (c3:
65 C).(csubst1 i v c1 c3))))) (let H5 \def (eq_ind_r nat x1 (\lambda (n:
66 nat).(subst0 n v u1 x0)) H4 i (s_inj k i x1 H2)) in (ex3_2_intro T C (\lambda
67 (u2: T).(\lambda (c3: C).(eq C (CHead c1 k x0) (CHead c3 k u2)))) (\lambda
68 (u2: T).(\lambda (_: C).(subst1 i v u1 u2))) (\lambda (_: T).(\lambda (c3:
69 C).(csubst1 i v c1 c3))) x0 c1 (refl_equal C (CHead c1 k x0)) (subst1_single
70 i v u1 x0 H5) (csubst1_refl i v c1))) c2 H3)))))) H1)) (\lambda (H1: (ex3_2 C
71 nat (\lambda (_: C).(\lambda (j: nat).(eq nat (s k i) (s k j)))) (\lambda
72 (c3: C).(\lambda (_: nat).(eq C c2 (CHead c3 k u1)))) (\lambda (c3:
73 C).(\lambda (j: nat).(csubst0 j v c1 c3))))).(ex3_2_ind C nat (\lambda (_:
74 C).(\lambda (j: nat).(eq nat (s k i) (s k j)))) (\lambda (c3: C).(\lambda (_:
75 nat).(eq C c2 (CHead c3 k u1)))) (\lambda (c3: C).(\lambda (j: nat).(csubst0
76 j v c1 c3))) (ex3_2 T C (\lambda (u2: T).(\lambda (c3: C).(eq C c2 (CHead c3
77 k u2)))) (\lambda (u2: T).(\lambda (_: C).(subst1 i v u1 u2))) (\lambda (_:
78 T).(\lambda (c3: C).(csubst1 i v c1 c3)))) (\lambda (x0: C).(\lambda (x1:
79 nat).(\lambda (H2: (eq nat (s k i) (s k x1))).(\lambda (H3: (eq C c2 (CHead
80 x0 k u1))).(\lambda (H4: (csubst0 x1 v c1 x0)).(eq_ind_r C (CHead x0 k u1)
81 (\lambda (c: C).(ex3_2 T C (\lambda (u2: T).(\lambda (c3: C).(eq C c (CHead
82 c3 k u2)))) (\lambda (u2: T).(\lambda (_: C).(subst1 i v u1 u2))) (\lambda
83 (_: T).(\lambda (c3: C).(csubst1 i v c1 c3))))) (let H5 \def (eq_ind_r nat x1
84 (\lambda (n: nat).(csubst0 n v c1 x0)) H4 i (s_inj k i x1 H2)) in
85 (ex3_2_intro T C (\lambda (u2: T).(\lambda (c3: C).(eq C (CHead x0 k u1)
86 (CHead c3 k u2)))) (\lambda (u2: T).(\lambda (_: C).(subst1 i v u1 u2)))
87 (\lambda (_: T).(\lambda (c3: C).(csubst1 i v c1 c3))) u1 x0 (refl_equal C
88 (CHead x0 k u1)) (subst1_refl i v u1) (csubst1_sing i v c1 x0 H5))) c2
89 H3)))))) H1)) (\lambda (H1: (ex4_3 T C nat (\lambda (_: T).(\lambda (_:
90 C).(\lambda (j: nat).(eq nat (s k i) (s k j))))) (\lambda (u2: T).(\lambda
91 (c3: C).(\lambda (_: nat).(eq C c2 (CHead c3 k u2))))) (\lambda (u2:
92 T).(\lambda (_: C).(\lambda (j: nat).(subst0 j v u1 u2)))) (\lambda (_:
93 T).(\lambda (c3: C).(\lambda (j: nat).(csubst0 j v c1 c3)))))).(ex4_3_ind T C
94 nat (\lambda (_: T).(\lambda (_: C).(\lambda (j: nat).(eq nat (s k i) (s k
95 j))))) (\lambda (u2: T).(\lambda (c3: C).(\lambda (_: nat).(eq C c2 (CHead c3
96 k u2))))) (\lambda (u2: T).(\lambda (_: C).(\lambda (j: nat).(subst0 j v u1
97 u2)))) (\lambda (_: T).(\lambda (c3: C).(\lambda (j: nat).(csubst0 j v c1
98 c3)))) (ex3_2 T C (\lambda (u2: T).(\lambda (c3: C).(eq C c2 (CHead c3 k
99 u2)))) (\lambda (u2: T).(\lambda (_: C).(subst1 i v u1 u2))) (\lambda (_:
100 T).(\lambda (c3: C).(csubst1 i v c1 c3)))) (\lambda (x0: T).(\lambda (x1:
101 C).(\lambda (x2: nat).(\lambda (H2: (eq nat (s k i) (s k x2))).(\lambda (H3:
102 (eq C c2 (CHead x1 k x0))).(\lambda (H4: (subst0 x2 v u1 x0)).(\lambda (H5:
103 (csubst0 x2 v c1 x1)).(eq_ind_r C (CHead x1 k x0) (\lambda (c: C).(ex3_2 T C
104 (\lambda (u2: T).(\lambda (c3: C).(eq C c (CHead c3 k u2)))) (\lambda (u2:
105 T).(\lambda (_: C).(subst1 i v u1 u2))) (\lambda (_: T).(\lambda (c3:
106 C).(csubst1 i v c1 c3))))) (let H6 \def (eq_ind_r nat x2 (\lambda (n:
107 nat).(csubst0 n v c1 x1)) H5 i (s_inj k i x2 H2)) in (let H7 \def (eq_ind_r
108 nat x2 (\lambda (n: nat).(subst0 n v u1 x0)) H4 i (s_inj k i x2 H2)) in
109 (ex3_2_intro T C (\lambda (u2: T).(\lambda (c3: C).(eq C (CHead x1 k x0)
110 (CHead c3 k u2)))) (\lambda (u2: T).(\lambda (_: C).(subst1 i v u1 u2)))
111 (\lambda (_: T).(\lambda (c3: C).(csubst1 i v c1 c3))) x0 x1 (refl_equal C
112 (CHead x1 k x0)) (subst1_single i v u1 x0 H7) (csubst1_sing i v c1 x1 H6))))
113 c2 H3)))))))) H1)) (csubst0_gen_head k c1 c2 u1 v (s k i) H0)))) x H))))))).