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 set "baseuri" "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/lift1/fwd".
19 include "lift1/defs.ma".
21 include "lift/fwd.ma".
24 \forall (hds: PList).(\forall (i: nat).(eq T (lift1 hds (TLRef i)) (TLRef
27 \lambda (hds: PList).(PList_ind (\lambda (p: PList).(\forall (i: nat).(eq T
28 (lift1 p (TLRef i)) (TLRef (trans p i))))) (\lambda (i: nat).(refl_equal T
29 (TLRef (trans PNil i)))) (\lambda (h: nat).(\lambda (d: nat).(\lambda (p:
30 PList).(\lambda (H: ((\forall (i: nat).(eq T (lift1 p (TLRef i)) (TLRef
31 (trans p i)))))).(\lambda (i: nat).(eq_ind_r T (TLRef (trans p i)) (\lambda
32 (t: T).(eq T (lift h d t) (TLRef (match (blt (trans p i) d) with [true
33 \Rightarrow (trans p i) | false \Rightarrow (plus (trans p i) h)]))))
34 (refl_equal T (TLRef (match (blt (trans p i) d) with [true \Rightarrow (trans
35 p i) | false \Rightarrow (plus (trans p i) h)]))) (lift1 p (TLRef i)) (H
39 \forall (b: B).(\forall (hds: PList).(\forall (u: T).(\forall (t: T).(eq T
40 (lift1 hds (THead (Bind b) u t)) (THead (Bind b) (lift1 hds u) (lift1 (Ss
43 \lambda (b: B).(\lambda (hds: PList).(PList_ind (\lambda (p: PList).(\forall
44 (u: T).(\forall (t: T).(eq T (lift1 p (THead (Bind b) u t)) (THead (Bind b)
45 (lift1 p u) (lift1 (Ss p) t)))))) (\lambda (u: T).(\lambda (t: T).(refl_equal
46 T (THead (Bind b) (lift1 PNil u) (lift1 (Ss PNil) t))))) (\lambda (h:
47 nat).(\lambda (d: nat).(\lambda (p: PList).(\lambda (H: ((\forall (u:
48 T).(\forall (t: T).(eq T (lift1 p (THead (Bind b) u t)) (THead (Bind b)
49 (lift1 p u) (lift1 (Ss p) t))))))).(\lambda (u: T).(\lambda (t: T).(eq_ind_r
50 T (THead (Bind b) (lift1 p u) (lift1 (Ss p) t)) (\lambda (t0: T).(eq T (lift
51 h d t0) (THead (Bind b) (lift h d (lift1 p u)) (lift h (S d) (lift1 (Ss p)
52 t))))) (eq_ind_r T (THead (Bind b) (lift h d (lift1 p u)) (lift h (S d)
53 (lift1 (Ss p) t))) (\lambda (t0: T).(eq T t0 (THead (Bind b) (lift h d (lift1
54 p u)) (lift h (S d) (lift1 (Ss p) t))))) (refl_equal T (THead (Bind b) (lift
55 h d (lift1 p u)) (lift h (S d) (lift1 (Ss p) t)))) (lift h d (THead (Bind b)
56 (lift1 p u) (lift1 (Ss p) t))) (lift_bind b (lift1 p u) (lift1 (Ss p) t) h
57 d)) (lift1 p (THead (Bind b) u t)) (H u t)))))))) hds)).
60 \forall (f: F).(\forall (hds: PList).(\forall (u: T).(\forall (t: T).(eq T
61 (lift1 hds (THead (Flat f) u t)) (THead (Flat f) (lift1 hds u) (lift1 hds
64 \lambda (f: F).(\lambda (hds: PList).(PList_ind (\lambda (p: PList).(\forall
65 (u: T).(\forall (t: T).(eq T (lift1 p (THead (Flat f) u t)) (THead (Flat f)
66 (lift1 p u) (lift1 p t)))))) (\lambda (u: T).(\lambda (t: T).(refl_equal T
67 (THead (Flat f) (lift1 PNil u) (lift1 PNil t))))) (\lambda (h: nat).(\lambda
68 (d: nat).(\lambda (p: PList).(\lambda (H: ((\forall (u: T).(\forall (t:
69 T).(eq T (lift1 p (THead (Flat f) u t)) (THead (Flat f) (lift1 p u) (lift1 p
70 t))))))).(\lambda (u: T).(\lambda (t: T).(eq_ind_r T (THead (Flat f) (lift1 p
71 u) (lift1 p t)) (\lambda (t0: T).(eq T (lift h d t0) (THead (Flat f) (lift h
72 d (lift1 p u)) (lift h d (lift1 p t))))) (eq_ind_r T (THead (Flat f) (lift h
73 d (lift1 p u)) (lift h d (lift1 p t))) (\lambda (t0: T).(eq T t0 (THead (Flat
74 f) (lift h d (lift1 p u)) (lift h d (lift1 p t))))) (refl_equal T (THead
75 (Flat f) (lift h d (lift1 p u)) (lift h d (lift1 p t)))) (lift h d (THead
76 (Flat f) (lift1 p u) (lift1 p t))) (lift_flat f (lift1 p u) (lift1 p t) h d))
77 (lift1 p (THead (Flat f) u t)) (H u t)))))))) hds)).
79 theorem lift1_cons_tail:
80 \forall (t: T).(\forall (h: nat).(\forall (d: nat).(\forall (hds: PList).(eq
81 T (lift1 (PConsTail hds h d) t) (lift1 hds (lift h d t))))))
83 \lambda (t: T).(\lambda (h: nat).(\lambda (d: nat).(\lambda (hds:
84 PList).(PList_ind (\lambda (p: PList).(eq T (lift1 (PConsTail p h d) t)
85 (lift1 p (lift h d t)))) (refl_equal T (lift h d t)) (\lambda (n:
86 nat).(\lambda (n0: nat).(\lambda (p: PList).(\lambda (H: (eq T (lift1
87 (PConsTail p h d) t) (lift1 p (lift h d t)))).(eq_ind_r T (lift1 p (lift h d
88 t)) (\lambda (t0: T).(eq T (lift n n0 t0) (lift n n0 (lift1 p (lift h d
89 t))))) (refl_equal T (lift n n0 (lift1 p (lift h d t)))) (lift1 (PConsTail p
90 h d) t) H))))) hds)))).
93 \forall (f: F).(\forall (hds: PList).(\forall (t: T).(\forall (ts:
94 TList).(eq T (lift1 hds (THeads (Flat f) ts t)) (THeads (Flat f) (lifts1 hds
95 ts) (lift1 hds t))))))
97 \lambda (f: F).(\lambda (hds: PList).(\lambda (t: T).(\lambda (ts:
98 TList).(TList_ind (\lambda (t0: TList).(eq T (lift1 hds (THeads (Flat f) t0
99 t)) (THeads (Flat f) (lifts1 hds t0) (lift1 hds t)))) (refl_equal T (lift1
100 hds t)) (\lambda (t0: T).(\lambda (t1: TList).(\lambda (H: (eq T (lift1 hds
101 (THeads (Flat f) t1 t)) (THeads (Flat f) (lifts1 hds t1) (lift1 hds
102 t)))).(eq_ind_r T (THead (Flat f) (lift1 hds t0) (lift1 hds (THeads (Flat f)
103 t1 t))) (\lambda (t2: T).(eq T t2 (THead (Flat f) (lift1 hds t0) (THeads
104 (Flat f) (lifts1 hds t1) (lift1 hds t))))) (eq_ind_r T (THeads (Flat f)
105 (lifts1 hds t1) (lift1 hds t)) (\lambda (t2: T).(eq T (THead (Flat f) (lift1
106 hds t0) t2) (THead (Flat f) (lift1 hds t0) (THeads (Flat f) (lifts1 hds t1)
107 (lift1 hds t))))) (refl_equal T (THead (Flat f) (lift1 hds t0) (THeads (Flat
108 f) (lifts1 hds t1) (lift1 hds t)))) (lift1 hds (THeads (Flat f) t1 t)) H)
109 (lift1 hds (THead (Flat f) t0 (THeads (Flat f) t1 t))) (lift1_flat f hds t0
110 (THeads (Flat f) t1 t)))))) ts)))).
113 \forall (ts: TList).(eq TList (lifts1 PNil ts) ts)
115 \lambda (ts: TList).(TList_ind (\lambda (t: TList).(eq TList (lifts1 PNil t)
116 t)) (refl_equal TList TNil) (\lambda (t: T).(\lambda (t0: TList).(\lambda (H:
117 (eq TList (lifts1 PNil t0) t0)).(eq_ind_r TList t0 (\lambda (t1: TList).(eq
118 TList (TCons t t1) (TCons t t0))) (refl_equal TList (TCons t t0)) (lifts1
122 \forall (h: nat).(\forall (d: nat).(\forall (hds: PList).(\forall (ts:
123 TList).(eq TList (lifts1 (PCons h d hds) ts) (lifts h d (lifts1 hds ts))))))
125 \lambda (h: nat).(\lambda (d: nat).(\lambda (hds: PList).(\lambda (ts:
126 TList).(TList_ind (\lambda (t: TList).(eq TList (lifts1 (PCons h d hds) t)
127 (lifts h d (lifts1 hds t)))) (refl_equal TList TNil) (\lambda (t: T).(\lambda
128 (t0: TList).(\lambda (H: (eq TList (lifts1 (PCons h d hds) t0) (lifts h d
129 (lifts1 hds t0)))).(eq_ind_r TList (lifts h d (lifts1 hds t0)) (\lambda (t1:
130 TList).(eq TList (TCons (lift h d (lift1 hds t)) t1) (TCons (lift h d (lift1
131 hds t)) (lifts h d (lifts1 hds t0))))) (refl_equal TList (TCons (lift h d
132 (lift1 hds t)) (lifts h d (lifts1 hds t0)))) (lifts1 (PCons h d hds) t0)