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