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/subst1/defs.ma".
19 include "LambdaDelta-1/subst0/props.ma".
21 theorem subst1_gen_sort:
22 \forall (v: T).(\forall (x: T).(\forall (i: nat).(\forall (n: nat).((subst1
23 i v (TSort n) x) \to (eq T x (TSort n))))))
25 \lambda (v: T).(\lambda (x: T).(\lambda (i: nat).(\lambda (n: nat).(\lambda
26 (H: (subst1 i v (TSort n) x)).(subst1_ind i v (TSort n) (\lambda (t: T).(eq T
27 t (TSort n))) (refl_equal T (TSort n)) (\lambda (t2: T).(\lambda (H0: (subst0
28 i v (TSort n) t2)).(subst0_gen_sort v t2 i n H0 (eq T t2 (TSort n))))) x
31 theorem subst1_gen_lref:
32 \forall (v: T).(\forall (x: T).(\forall (i: nat).(\forall (n: nat).((subst1
33 i v (TLRef n) x) \to (or (eq T x (TLRef n)) (land (eq nat n i) (eq T x (lift
36 \lambda (v: T).(\lambda (x: T).(\lambda (i: nat).(\lambda (n: nat).(\lambda
37 (H: (subst1 i v (TLRef n) x)).(subst1_ind i v (TLRef n) (\lambda (t: T).(or
38 (eq T t (TLRef n)) (land (eq nat n i) (eq T t (lift (S n) O v))))) (or_introl
39 (eq T (TLRef n) (TLRef n)) (land (eq nat n i) (eq T (TLRef n) (lift (S n) O
40 v))) (refl_equal T (TLRef n))) (\lambda (t2: T).(\lambda (H0: (subst0 i v
41 (TLRef n) t2)).(land_ind (eq nat n i) (eq T t2 (lift (S n) O v)) (or (eq T t2
42 (TLRef n)) (land (eq nat n i) (eq T t2 (lift (S n) O v)))) (\lambda (H1: (eq
43 nat n i)).(\lambda (H2: (eq T t2 (lift (S n) O v))).(or_intror (eq T t2
44 (TLRef n)) (land (eq nat n i) (eq T t2 (lift (S n) O v))) (conj (eq nat n i)
45 (eq T t2 (lift (S n) O v)) H1 H2)))) (subst0_gen_lref v t2 i n H0)))) x
48 theorem subst1_gen_head:
49 \forall (k: K).(\forall (v: T).(\forall (u1: T).(\forall (t1: T).(\forall
50 (x: T).(\forall (i: nat).((subst1 i v (THead k u1 t1) x) \to (ex3_2 T T
51 (\lambda (u2: T).(\lambda (t2: T).(eq T x (THead k u2 t2)))) (\lambda (u2:
52 T).(\lambda (_: T).(subst1 i v u1 u2))) (\lambda (_: T).(\lambda (t2:
53 T).(subst1 (s k i) v t1 t2))))))))))
55 \lambda (k: K).(\lambda (v: T).(\lambda (u1: T).(\lambda (t1: T).(\lambda
56 (x: T).(\lambda (i: nat).(\lambda (H: (subst1 i v (THead k u1 t1)
57 x)).(subst1_ind i v (THead k u1 t1) (\lambda (t: T).(ex3_2 T T (\lambda (u2:
58 T).(\lambda (t2: T).(eq T t (THead k u2 t2)))) (\lambda (u2: T).(\lambda (_:
59 T).(subst1 i v u1 u2))) (\lambda (_: T).(\lambda (t2: T).(subst1 (s k i) v t1
60 t2))))) (ex3_2_intro T T (\lambda (u2: T).(\lambda (t2: T).(eq T (THead k u1
61 t1) (THead k u2 t2)))) (\lambda (u2: T).(\lambda (_: T).(subst1 i v u1 u2)))
62 (\lambda (_: T).(\lambda (t2: T).(subst1 (s k i) v t1 t2))) u1 t1 (refl_equal
63 T (THead k u1 t1)) (subst1_refl i v u1) (subst1_refl (s k i) v t1)) (\lambda
64 (t2: T).(\lambda (H0: (subst0 i v (THead k u1 t1) t2)).(or3_ind (ex2 T
65 (\lambda (u2: T).(eq T t2 (THead k u2 t1))) (\lambda (u2: T).(subst0 i v u1
66 u2))) (ex2 T (\lambda (t3: T).(eq T t2 (THead k u1 t3))) (\lambda (t3:
67 T).(subst0 (s k i) v t1 t3))) (ex3_2 T T (\lambda (u2: T).(\lambda (t3:
68 T).(eq T t2 (THead k u2 t3)))) (\lambda (u2: T).(\lambda (_: T).(subst0 i v
69 u1 u2))) (\lambda (_: T).(\lambda (t3: T).(subst0 (s k i) v t1 t3)))) (ex3_2
70 T T (\lambda (u2: T).(\lambda (t3: T).(eq T t2 (THead k u2 t3)))) (\lambda
71 (u2: T).(\lambda (_: T).(subst1 i v u1 u2))) (\lambda (_: T).(\lambda (t3:
72 T).(subst1 (s k i) v t1 t3)))) (\lambda (H1: (ex2 T (\lambda (u2: T).(eq T t2
73 (THead k u2 t1))) (\lambda (u2: T).(subst0 i v u1 u2)))).(ex2_ind T (\lambda
74 (u2: T).(eq T t2 (THead k u2 t1))) (\lambda (u2: T).(subst0 i v u1 u2))
75 (ex3_2 T T (\lambda (u2: T).(\lambda (t3: T).(eq T t2 (THead k u2 t3))))
76 (\lambda (u2: T).(\lambda (_: T).(subst1 i v u1 u2))) (\lambda (_:
77 T).(\lambda (t3: T).(subst1 (s k i) v t1 t3)))) (\lambda (x0: T).(\lambda
78 (H2: (eq T t2 (THead k x0 t1))).(\lambda (H3: (subst0 i v u1
79 x0)).(ex3_2_intro T T (\lambda (u2: T).(\lambda (t3: T).(eq T t2 (THead k u2
80 t3)))) (\lambda (u2: T).(\lambda (_: T).(subst1 i v u1 u2))) (\lambda (_:
81 T).(\lambda (t3: T).(subst1 (s k i) v t1 t3))) x0 t1 H2 (subst1_single i v u1
82 x0 H3) (subst1_refl (s k i) v t1))))) H1)) (\lambda (H1: (ex2 T (\lambda (t3:
83 T).(eq T t2 (THead k u1 t3))) (\lambda (t3: T).(subst0 (s k i) v t1
84 t3)))).(ex2_ind T (\lambda (t3: T).(eq T t2 (THead k u1 t3))) (\lambda (t3:
85 T).(subst0 (s k i) v t1 t3)) (ex3_2 T T (\lambda (u2: T).(\lambda (t3: T).(eq
86 T t2 (THead k u2 t3)))) (\lambda (u2: T).(\lambda (_: T).(subst1 i v u1 u2)))
87 (\lambda (_: T).(\lambda (t3: T).(subst1 (s k i) v t1 t3)))) (\lambda (x0:
88 T).(\lambda (H2: (eq T t2 (THead k u1 x0))).(\lambda (H3: (subst0 (s k i) v
89 t1 x0)).(ex3_2_intro T T (\lambda (u2: T).(\lambda (t3: T).(eq T t2 (THead k
90 u2 t3)))) (\lambda (u2: T).(\lambda (_: T).(subst1 i v u1 u2))) (\lambda (_:
91 T).(\lambda (t3: T).(subst1 (s k i) v t1 t3))) u1 x0 H2 (subst1_refl i v u1)
92 (subst1_single (s k i) v t1 x0 H3))))) H1)) (\lambda (H1: (ex3_2 T T (\lambda
93 (u2: T).(\lambda (t3: T).(eq T t2 (THead k u2 t3)))) (\lambda (u2:
94 T).(\lambda (_: T).(subst0 i v u1 u2))) (\lambda (_: T).(\lambda (t3:
95 T).(subst0 (s k i) v t1 t3))))).(ex3_2_ind T T (\lambda (u2: T).(\lambda (t3:
96 T).(eq T t2 (THead k u2 t3)))) (\lambda (u2: T).(\lambda (_: T).(subst0 i v
97 u1 u2))) (\lambda (_: T).(\lambda (t3: T).(subst0 (s k i) v t1 t3))) (ex3_2 T
98 T (\lambda (u2: T).(\lambda (t3: T).(eq T t2 (THead k u2 t3)))) (\lambda (u2:
99 T).(\lambda (_: T).(subst1 i v u1 u2))) (\lambda (_: T).(\lambda (t3:
100 T).(subst1 (s k i) v t1 t3)))) (\lambda (x0: T).(\lambda (x1: T).(\lambda
101 (H2: (eq T t2 (THead k x0 x1))).(\lambda (H3: (subst0 i v u1 x0)).(\lambda
102 (H4: (subst0 (s k i) v t1 x1)).(ex3_2_intro T T (\lambda (u2: T).(\lambda
103 (t3: T).(eq T t2 (THead k u2 t3)))) (\lambda (u2: T).(\lambda (_: T).(subst1
104 i v u1 u2))) (\lambda (_: T).(\lambda (t3: T).(subst1 (s k i) v t1 t3))) x0
105 x1 H2 (subst1_single i v u1 x0 H3) (subst1_single (s k i) v t1 x1 H4)))))))
106 H1)) (subst0_gen_head k v u1 t1 t2 i H0)))) x H))))))).
108 theorem subst1_gen_lift_lt:
109 \forall (u: T).(\forall (t1: T).(\forall (x: T).(\forall (i: nat).(\forall
110 (h: nat).(\forall (d: nat).((subst1 i (lift h d u) (lift h (S (plus i d)) t1)
111 x) \to (ex2 T (\lambda (t2: T).(eq T x (lift h (S (plus i d)) t2))) (\lambda
112 (t2: T).(subst1 i u t1 t2)))))))))
114 \lambda (u: T).(\lambda (t1: T).(\lambda (x: T).(\lambda (i: nat).(\lambda
115 (h: nat).(\lambda (d: nat).(\lambda (H: (subst1 i (lift h d u) (lift h (S
116 (plus i d)) t1) x)).(subst1_ind i (lift h d u) (lift h (S (plus i d)) t1)
117 (\lambda (t: T).(ex2 T (\lambda (t2: T).(eq T t (lift h (S (plus i d)) t2)))
118 (\lambda (t2: T).(subst1 i u t1 t2)))) (ex_intro2 T (\lambda (t2: T).(eq T
119 (lift h (S (plus i d)) t1) (lift h (S (plus i d)) t2))) (\lambda (t2:
120 T).(subst1 i u t1 t2)) t1 (refl_equal T (lift h (S (plus i d)) t1))
121 (subst1_refl i u t1)) (\lambda (t2: T).(\lambda (H0: (subst0 i (lift h d u)
122 (lift h (S (plus i d)) t1) t2)).(ex2_ind T (\lambda (t3: T).(eq T t2 (lift h
123 (S (plus i d)) t3))) (\lambda (t3: T).(subst0 i u t1 t3)) (ex2 T (\lambda
124 (t3: T).(eq T t2 (lift h (S (plus i d)) t3))) (\lambda (t3: T).(subst1 i u t1
125 t3))) (\lambda (x0: T).(\lambda (H1: (eq T t2 (lift h (S (plus i d))
126 x0))).(\lambda (H2: (subst0 i u t1 x0)).(ex_intro2 T (\lambda (t3: T).(eq T
127 t2 (lift h (S (plus i d)) t3))) (\lambda (t3: T).(subst1 i u t1 t3)) x0 H1
128 (subst1_single i u t1 x0 H2))))) (subst0_gen_lift_lt u t1 t2 i h d H0)))) x
131 theorem subst1_gen_lift_eq:
132 \forall (t: T).(\forall (u: T).(\forall (x: T).(\forall (h: nat).(\forall
133 (d: nat).(\forall (i: nat).((le d i) \to ((lt i (plus d h)) \to ((subst1 i u
134 (lift h d t) x) \to (eq T x (lift h d t))))))))))
136 \lambda (t: T).(\lambda (u: T).(\lambda (x: T).(\lambda (h: nat).(\lambda
137 (d: nat).(\lambda (i: nat).(\lambda (H: (le d i)).(\lambda (H0: (lt i (plus d
138 h))).(\lambda (H1: (subst1 i u (lift h d t) x)).(subst1_ind i u (lift h d t)
139 (\lambda (t0: T).(eq T t0 (lift h d t))) (refl_equal T (lift h d t)) (\lambda
140 (t2: T).(\lambda (H2: (subst0 i u (lift h d t) t2)).(subst0_gen_lift_false t
141 u t2 h d i H H0 H2 (eq T t2 (lift h d t))))) x H1))))))))).
143 theorem subst1_gen_lift_ge:
144 \forall (u: T).(\forall (t1: T).(\forall (x: T).(\forall (i: nat).(\forall
145 (h: nat).(\forall (d: nat).((subst1 i u (lift h d t1) x) \to ((le (plus d h)
146 i) \to (ex2 T (\lambda (t2: T).(eq T x (lift h d t2))) (\lambda (t2:
147 T).(subst1 (minus i h) u t1 t2))))))))))
149 \lambda (u: T).(\lambda (t1: T).(\lambda (x: T).(\lambda (i: nat).(\lambda
150 (h: nat).(\lambda (d: nat).(\lambda (H: (subst1 i u (lift h d t1)
151 x)).(\lambda (H0: (le (plus d h) i)).(subst1_ind i u (lift h d t1) (\lambda
152 (t: T).(ex2 T (\lambda (t2: T).(eq T t (lift h d t2))) (\lambda (t2:
153 T).(subst1 (minus i h) u t1 t2)))) (ex_intro2 T (\lambda (t2: T).(eq T (lift
154 h d t1) (lift h d t2))) (\lambda (t2: T).(subst1 (minus i h) u t1 t2)) t1
155 (refl_equal T (lift h d t1)) (subst1_refl (minus i h) u t1)) (\lambda (t2:
156 T).(\lambda (H1: (subst0 i u (lift h d t1) t2)).(ex2_ind T (\lambda (t3:
157 T).(eq T t2 (lift h d t3))) (\lambda (t3: T).(subst0 (minus i h) u t1 t3))
158 (ex2 T (\lambda (t3: T).(eq T t2 (lift h d t3))) (\lambda (t3: T).(subst1
159 (minus i h) u t1 t3))) (\lambda (x0: T).(\lambda (H2: (eq T t2 (lift h d
160 x0))).(\lambda (H3: (subst0 (minus i h) u t1 x0)).(ex_intro2 T (\lambda (t3:
161 T).(eq T t2 (lift h d t3))) (\lambda (t3: T).(subst1 (minus i h) u t1 t3)) x0
162 H2 (subst1_single (minus i h) u t1 x0 H3))))) (subst0_gen_lift_ge u t1 t2 i h
163 d H1 H0)))) x H)))))))).