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/props.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)).
31 \forall (hds: PList).(\forall (i: nat).(eq T (lift1 hds (TLRef i)) (TLRef
34 \lambda (hds: PList).(PList_ind (\lambda (p: PList).(\forall (i: nat).(eq T
35 (lift1 p (TLRef i)) (TLRef (trans p i))))) (\lambda (i: nat).(refl_equal T
36 (TLRef i))) (\lambda (n: nat).(\lambda (n0: nat).(\lambda (p: PList).(\lambda
37 (H: ((\forall (i: nat).(eq T (lift1 p (TLRef i)) (TLRef (trans p
38 i)))))).(\lambda (i: nat).(eq_ind_r T (TLRef (trans p i)) (\lambda (t: T).(eq
39 T (lift n n0 t) (TLRef (match (blt (trans p i) n0) with [true \Rightarrow
40 (trans p i) | false \Rightarrow (plus (trans p i) n)])))) (refl_equal T
41 (TLRef (match (blt (trans p i) n0) with [true \Rightarrow (trans p i) | false
42 \Rightarrow (plus (trans p i) n)]))) (lift1 p (TLRef i)) (H i))))))) hds).
45 \forall (b: B).(\forall (hds: PList).(\forall (u: T).(\forall (t: T).(eq T
46 (lift1 hds (THead (Bind b) u t)) (THead (Bind b) (lift1 hds u) (lift1 (Ss
49 \lambda (b: B).(\lambda (hds: PList).(PList_ind (\lambda (p: PList).(\forall
50 (u: T).(\forall (t: T).(eq T (lift1 p (THead (Bind b) u t)) (THead (Bind b)
51 (lift1 p u) (lift1 (Ss p) t)))))) (\lambda (u: T).(\lambda (t: T).(refl_equal
52 T (THead (Bind b) u t)))) (\lambda (n: nat).(\lambda (n0: nat).(\lambda (p:
53 PList).(\lambda (H: ((\forall (u: T).(\forall (t: T).(eq T (lift1 p (THead
54 (Bind b) u t)) (THead (Bind b) (lift1 p u) (lift1 (Ss p) t))))))).(\lambda
55 (u: T).(\lambda (t: T).(eq_ind_r T (THead (Bind b) (lift1 p u) (lift1 (Ss p)
56 t)) (\lambda (t0: T).(eq T (lift n n0 t0) (THead (Bind b) (lift n n0 (lift1 p
57 u)) (lift n (S n0) (lift1 (Ss p) t))))) (eq_ind_r T (THead (Bind b) (lift n
58 n0 (lift1 p u)) (lift n (S n0) (lift1 (Ss p) t))) (\lambda (t0: T).(eq T t0
59 (THead (Bind b) (lift n n0 (lift1 p u)) (lift n (S n0) (lift1 (Ss p) t)))))
60 (refl_equal T (THead (Bind b) (lift n n0 (lift1 p u)) (lift n (S n0) (lift1
61 (Ss p) t)))) (lift n n0 (THead (Bind b) (lift1 p u) (lift1 (Ss p) t)))
62 (lift_bind b (lift1 p u) (lift1 (Ss p) t) n n0)) (lift1 p (THead (Bind b) u
63 t)) (H u t)))))))) hds)).
66 \forall (f: F).(\forall (hds: PList).(\forall (u: T).(\forall (t: T).(eq T
67 (lift1 hds (THead (Flat f) u t)) (THead (Flat f) (lift1 hds u) (lift1 hds
70 \lambda (f: F).(\lambda (hds: PList).(PList_ind (\lambda (p: PList).(\forall
71 (u: T).(\forall (t: T).(eq T (lift1 p (THead (Flat f) u t)) (THead (Flat f)
72 (lift1 p u) (lift1 p t)))))) (\lambda (u: T).(\lambda (t: T).(refl_equal T
73 (THead (Flat f) u t)))) (\lambda (n: nat).(\lambda (n0: nat).(\lambda (p:
74 PList).(\lambda (H: ((\forall (u: T).(\forall (t: T).(eq T (lift1 p (THead
75 (Flat f) u t)) (THead (Flat f) (lift1 p u) (lift1 p t))))))).(\lambda (u:
76 T).(\lambda (t: T).(eq_ind_r T (THead (Flat f) (lift1 p u) (lift1 p t))
77 (\lambda (t0: T).(eq T (lift n n0 t0) (THead (Flat f) (lift n n0 (lift1 p u))
78 (lift n n0 (lift1 p t))))) (eq_ind_r T (THead (Flat f) (lift n n0 (lift1 p
79 u)) (lift n n0 (lift1 p t))) (\lambda (t0: T).(eq T t0 (THead (Flat f) (lift
80 n n0 (lift1 p u)) (lift n n0 (lift1 p t))))) (refl_equal T (THead (Flat f)
81 (lift n n0 (lift1 p u)) (lift n n0 (lift1 p t)))) (lift n n0 (THead (Flat f)
82 (lift1 p u) (lift1 p t))) (lift_flat f (lift1 p u) (lift1 p t) n n0)) (lift1
83 p (THead (Flat f) u t)) (H u t)))))))) hds)).
85 lemma lift1_cons_tail:
86 \forall (t: T).(\forall (h: nat).(\forall (d: nat).(\forall (hds: PList).(eq
87 T (lift1 (PConsTail hds h d) t) (lift1 hds (lift h d t))))))
89 \lambda (t: T).(\lambda (h: nat).(\lambda (d: nat).(\lambda (hds:
90 PList).(PList_ind (\lambda (p: PList).(eq T (lift1 (PConsTail p h d) t)
91 (lift1 p (lift h d t)))) (refl_equal T (lift h d t)) (\lambda (n:
92 nat).(\lambda (n0: nat).(\lambda (p: PList).(\lambda (H: (eq T (lift1
93 (PConsTail p h d) t) (lift1 p (lift h d t)))).(eq_ind_r T (lift1 p (lift h d
94 t)) (\lambda (t0: T).(eq T (lift n n0 t0) (lift n n0 (lift1 p (lift h d
95 t))))) (refl_equal T (lift n n0 (lift1 p (lift h d t)))) (lift1 (PConsTail p
96 h d) t) H))))) hds)))).
99 \forall (f: F).(\forall (hds: PList).(\forall (t: T).(\forall (ts:
100 TList).(eq T (lift1 hds (THeads (Flat f) ts t)) (THeads (Flat f) (lifts1 hds
101 ts) (lift1 hds t))))))
103 \lambda (f: F).(\lambda (hds: PList).(\lambda (t: T).(\lambda (ts:
104 TList).(TList_ind (\lambda (t0: TList).(eq T (lift1 hds (THeads (Flat f) t0
105 t)) (THeads (Flat f) (lifts1 hds t0) (lift1 hds t)))) (refl_equal T (lift1
106 hds t)) (\lambda (t0: T).(\lambda (t1: TList).(\lambda (H: (eq T (lift1 hds
107 (THeads (Flat f) t1 t)) (THeads (Flat f) (lifts1 hds t1) (lift1 hds
108 t)))).(eq_ind_r T (THead (Flat f) (lift1 hds t0) (lift1 hds (THeads (Flat f)
109 t1 t))) (\lambda (t2: T).(eq T t2 (THead (Flat f) (lift1 hds t0) (THeads
110 (Flat f) (lifts1 hds t1) (lift1 hds t))))) (eq_ind_r T (THeads (Flat f)
111 (lifts1 hds t1) (lift1 hds t)) (\lambda (t2: T).(eq T (THead (Flat f) (lift1
112 hds t0) t2) (THead (Flat f) (lift1 hds t0) (THeads (Flat f) (lifts1 hds t1)
113 (lift1 hds t))))) (refl_equal T (THead (Flat f) (lift1 hds t0) (THeads (Flat
114 f) (lifts1 hds t1) (lift1 hds t)))) (lift1 hds (THeads (Flat f) t1 t)) H)
115 (lift1 hds (THead (Flat f) t0 (THeads (Flat f) t1 t))) (lift1_flat f hds t0
116 (THeads (Flat f) t1 t)))))) ts)))).
119 \forall (ts: TList).(eq TList (lifts1 PNil ts) ts)
121 \lambda (ts: TList).(TList_ind (\lambda (t: TList).(eq TList (lifts1 PNil t)
122 t)) (refl_equal TList TNil) (\lambda (t: T).(\lambda (t0: TList).(\lambda (H:
123 (eq TList (lifts1 PNil t0) t0)).(eq_ind_r TList t0 (\lambda (t1: TList).(eq
124 TList (TCons t t1) (TCons t t0))) (refl_equal TList (TCons t t0)) (lifts1
128 \forall (h: nat).(\forall (d: nat).(\forall (hds: PList).(\forall (ts:
129 TList).(eq TList (lifts1 (PCons h d hds) ts) (lifts h d (lifts1 hds ts))))))
131 \lambda (h: nat).(\lambda (d: nat).(\lambda (hds: PList).(\lambda (ts:
132 TList).(TList_ind (\lambda (t: TList).(eq TList (lifts1 (PCons h d hds) t)
133 (lifts h d (lifts1 hds t)))) (refl_equal TList TNil) (\lambda (t: T).(\lambda
134 (t0: TList).(\lambda (H: (eq TList (lifts1 (PCons h d hds) t0) (lifts h d
135 (lifts1 hds t0)))).(eq_ind_r TList (lifts h d (lifts1 hds t0)) (\lambda (t1:
136 TList).(eq TList (TCons (lift h d (lift1 hds t)) t1) (TCons (lift h d (lift1
137 hds t)) (lifts h d (lifts1 hds t0))))) (refl_equal TList (TCons (lift h d
138 (lift1 hds t)) (lifts h d (lifts1 hds t0)))) (lifts1 (PCons h d hds) t0)