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-1/lift1/defs.ma".
19 include "Basic-1/lift/fwd.ma".
22 \forall (n: nat).(\forall (is: PList).(eq T (lift1 is (TSort n)) (TSort n)))
24 \lambda (n: nat).(\lambda (is: PList).(PList_ind (\lambda (p: PList).(eq T
25 (lift1 p (TSort n)) (TSort n))) (refl_equal T (TSort n)) (\lambda (n0:
26 nat).(\lambda (n1: nat).(\lambda (p: PList).(\lambda (H: (eq T (lift1 p
27 (TSort n)) (TSort n))).(eq_ind_r T (TSort n) (\lambda (t: T).(eq T (lift n0
28 n1 t) (TSort n))) (refl_equal T (TSort n)) (lift1 p (TSort n)) H))))) is)).
34 \forall (hds: PList).(\forall (i: nat).(eq T (lift1 hds (TLRef i)) (TLRef
37 \lambda (hds: PList).(PList_ind (\lambda (p: PList).(\forall (i: nat).(eq T
38 (lift1 p (TLRef i)) (TLRef (trans p i))))) (\lambda (i: nat).(refl_equal T
39 (TLRef i))) (\lambda (n: nat).(\lambda (n0: nat).(\lambda (p: PList).(\lambda
40 (H: ((\forall (i: nat).(eq T (lift1 p (TLRef i)) (TLRef (trans p
41 i)))))).(\lambda (i: nat).(eq_ind_r T (TLRef (trans p i)) (\lambda (t: T).(eq
42 T (lift n n0 t) (TLRef (match (blt (trans p i) n0) with [true \Rightarrow
43 (trans p i) | false \Rightarrow (plus (trans p i) n)])))) (refl_equal T
44 (TLRef (match (blt (trans p i) n0) with [true \Rightarrow (trans p i) | false
45 \Rightarrow (plus (trans p i) n)]))) (lift1 p (TLRef i)) (H i))))))) hds).
51 \forall (b: B).(\forall (hds: PList).(\forall (u: T).(\forall (t: T).(eq T
52 (lift1 hds (THead (Bind b) u t)) (THead (Bind b) (lift1 hds u) (lift1 (Ss
55 \lambda (b: B).(\lambda (hds: PList).(PList_ind (\lambda (p: PList).(\forall
56 (u: T).(\forall (t: T).(eq T (lift1 p (THead (Bind b) u t)) (THead (Bind b)
57 (lift1 p u) (lift1 (Ss p) t)))))) (\lambda (u: T).(\lambda (t: T).(refl_equal
58 T (THead (Bind b) u t)))) (\lambda (n: nat).(\lambda (n0: nat).(\lambda (p:
59 PList).(\lambda (H: ((\forall (u: T).(\forall (t: T).(eq T (lift1 p (THead
60 (Bind b) u t)) (THead (Bind b) (lift1 p u) (lift1 (Ss p) t))))))).(\lambda
61 (u: T).(\lambda (t: T).(eq_ind_r T (THead (Bind b) (lift1 p u) (lift1 (Ss p)
62 t)) (\lambda (t0: T).(eq T (lift n n0 t0) (THead (Bind b) (lift n n0 (lift1 p
63 u)) (lift n (S n0) (lift1 (Ss p) t))))) (eq_ind_r T (THead (Bind b) (lift n
64 n0 (lift1 p u)) (lift n (S n0) (lift1 (Ss p) t))) (\lambda (t0: T).(eq T t0
65 (THead (Bind b) (lift n n0 (lift1 p u)) (lift n (S n0) (lift1 (Ss p) t)))))
66 (refl_equal T (THead (Bind b) (lift n n0 (lift1 p u)) (lift n (S n0) (lift1
67 (Ss p) t)))) (lift n n0 (THead (Bind b) (lift1 p u) (lift1 (Ss p) t)))
68 (lift_bind b (lift1 p u) (lift1 (Ss p) t) n n0)) (lift1 p (THead (Bind b) u
69 t)) (H u t)))))))) hds)).
75 \forall (f: F).(\forall (hds: PList).(\forall (u: T).(\forall (t: T).(eq T
76 (lift1 hds (THead (Flat f) u t)) (THead (Flat f) (lift1 hds u) (lift1 hds
79 \lambda (f: F).(\lambda (hds: PList).(PList_ind (\lambda (p: PList).(\forall
80 (u: T).(\forall (t: T).(eq T (lift1 p (THead (Flat f) u t)) (THead (Flat f)
81 (lift1 p u) (lift1 p t)))))) (\lambda (u: T).(\lambda (t: T).(refl_equal T
82 (THead (Flat f) u t)))) (\lambda (n: nat).(\lambda (n0: nat).(\lambda (p:
83 PList).(\lambda (H: ((\forall (u: T).(\forall (t: T).(eq T (lift1 p (THead
84 (Flat f) u t)) (THead (Flat f) (lift1 p u) (lift1 p t))))))).(\lambda (u:
85 T).(\lambda (t: T).(eq_ind_r T (THead (Flat f) (lift1 p u) (lift1 p t))
86 (\lambda (t0: T).(eq T (lift n n0 t0) (THead (Flat f) (lift n n0 (lift1 p u))
87 (lift n n0 (lift1 p t))))) (eq_ind_r T (THead (Flat f) (lift n n0 (lift1 p
88 u)) (lift n n0 (lift1 p t))) (\lambda (t0: T).(eq T t0 (THead (Flat f) (lift
89 n n0 (lift1 p u)) (lift n n0 (lift1 p t))))) (refl_equal T (THead (Flat f)
90 (lift n n0 (lift1 p u)) (lift n n0 (lift1 p t)))) (lift n n0 (THead (Flat f)
91 (lift1 p u) (lift1 p t))) (lift_flat f (lift1 p u) (lift1 p t) n n0)) (lift1
92 p (THead (Flat f) u t)) (H u t)))))))) hds)).
97 theorem lift1_cons_tail:
98 \forall (t: T).(\forall (h: nat).(\forall (d: nat).(\forall (hds: PList).(eq
99 T (lift1 (PConsTail hds h d) t) (lift1 hds (lift h d t))))))
101 \lambda (t: T).(\lambda (h: nat).(\lambda (d: nat).(\lambda (hds:
102 PList).(PList_ind (\lambda (p: PList).(eq T (lift1 (PConsTail p h d) t)
103 (lift1 p (lift h d t)))) (refl_equal T (lift h d t)) (\lambda (n:
104 nat).(\lambda (n0: nat).(\lambda (p: PList).(\lambda (H: (eq T (lift1
105 (PConsTail p h d) t) (lift1 p (lift h d t)))).(eq_ind_r T (lift1 p (lift h d
106 t)) (\lambda (t0: T).(eq T (lift n n0 t0) (lift n n0 (lift1 p (lift h d
107 t))))) (refl_equal T (lift n n0 (lift1 p (lift h d t)))) (lift1 (PConsTail p
108 h d) t) H))))) hds)))).
114 \forall (f: F).(\forall (hds: PList).(\forall (t: T).(\forall (ts:
115 TList).(eq T (lift1 hds (THeads (Flat f) ts t)) (THeads (Flat f) (lifts1 hds
116 ts) (lift1 hds t))))))
118 \lambda (f: F).(\lambda (hds: PList).(\lambda (t: T).(\lambda (ts:
119 TList).(TList_ind (\lambda (t0: TList).(eq T (lift1 hds (THeads (Flat f) t0
120 t)) (THeads (Flat f) (lifts1 hds t0) (lift1 hds t)))) (refl_equal T (lift1
121 hds t)) (\lambda (t0: T).(\lambda (t1: TList).(\lambda (H: (eq T (lift1 hds
122 (THeads (Flat f) t1 t)) (THeads (Flat f) (lifts1 hds t1) (lift1 hds
123 t)))).(eq_ind_r T (THead (Flat f) (lift1 hds t0) (lift1 hds (THeads (Flat f)
124 t1 t))) (\lambda (t2: T).(eq T t2 (THead (Flat f) (lift1 hds t0) (THeads
125 (Flat f) (lifts1 hds t1) (lift1 hds t))))) (eq_ind_r T (THeads (Flat f)
126 (lifts1 hds t1) (lift1 hds t)) (\lambda (t2: T).(eq T (THead (Flat f) (lift1
127 hds t0) t2) (THead (Flat f) (lift1 hds t0) (THeads (Flat f) (lifts1 hds t1)
128 (lift1 hds t))))) (refl_equal T (THead (Flat f) (lift1 hds t0) (THeads (Flat
129 f) (lifts1 hds t1) (lift1 hds t)))) (lift1 hds (THeads (Flat f) t1 t)) H)
130 (lift1 hds (THead (Flat f) t0 (THeads (Flat f) t1 t))) (lift1_flat f hds t0
131 (THeads (Flat f) t1 t)))))) ts)))).
137 \forall (ts: TList).(eq TList (lifts1 PNil ts) ts)
139 \lambda (ts: TList).(TList_ind (\lambda (t: TList).(eq TList (lifts1 PNil t)
140 t)) (refl_equal TList TNil) (\lambda (t: T).(\lambda (t0: TList).(\lambda (H:
141 (eq TList (lifts1 PNil t0) t0)).(eq_ind_r TList t0 (\lambda (t1: TList).(eq
142 TList (TCons t t1) (TCons t t0))) (refl_equal TList (TCons t t0)) (lifts1
149 \forall (h: nat).(\forall (d: nat).(\forall (hds: PList).(\forall (ts:
150 TList).(eq TList (lifts1 (PCons h d hds) ts) (lifts h d (lifts1 hds ts))))))
152 \lambda (h: nat).(\lambda (d: nat).(\lambda (hds: PList).(\lambda (ts:
153 TList).(TList_ind (\lambda (t: TList).(eq TList (lifts1 (PCons h d hds) t)
154 (lifts h d (lifts1 hds t)))) (refl_equal TList TNil) (\lambda (t: T).(\lambda
155 (t0: TList).(\lambda (H: (eq TList (lifts1 (PCons h d hds) t0) (lifts h d
156 (lifts1 hds t0)))).(eq_ind_r TList (lifts h d (lifts1 hds t0)) (\lambda (t1:
157 TList).(eq TList (TCons (lift h d (lift1 hds t)) t1) (TCons (lift h d (lift1
158 hds t)) (lifts h d (lifts1 hds t0))))) (refl_equal TList (TCons (lift h d
159 (lift1 hds t)) (lifts h d (lifts1 hds t0)))) (lifts1 (PCons h d hds) t0)