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/LambdaDelta-1/lift1/fwd".
19 include "lift1/defs.ma".
21 include "lift/fwd.ma".
24 \forall (n: nat).(\forall (is: PList).(eq T (lift1 is (TSort n)) (TSort n)))
26 \lambda (n: nat).(\lambda (is: PList).(PList_ind (\lambda (p: PList).(eq T
27 (lift1 p (TSort n)) (TSort n))) (refl_equal T (TSort n)) (\lambda (n0:
28 nat).(\lambda (n1: nat).(\lambda (p: PList).(\lambda (H: (eq T (lift1 p
29 (TSort n)) (TSort n))).(eq_ind_r T (TSort n) (\lambda (t: T).(eq T (lift n0
30 n1 t) (TSort n))) (refl_equal T (TSort n)) (lift1 p (TSort n)) H))))) is)).
33 \forall (hds: PList).(\forall (i: nat).(eq T (lift1 hds (TLRef i)) (TLRef
36 \lambda (hds: PList).(PList_ind (\lambda (p: PList).(\forall (i: nat).(eq T
37 (lift1 p (TLRef i)) (TLRef (trans p i))))) (\lambda (i: nat).(refl_equal T
38 (TLRef i))) (\lambda (n: nat).(\lambda (n0: nat).(\lambda (p: PList).(\lambda
39 (H: ((\forall (i: nat).(eq T (lift1 p (TLRef i)) (TLRef (trans p
40 i)))))).(\lambda (i: nat).(eq_ind_r T (TLRef (trans p i)) (\lambda (t: T).(eq
41 T (lift n n0 t) (TLRef (match (blt (trans p i) n0) with [true \Rightarrow
42 (trans p i) | false \Rightarrow (plus (trans p i) n)])))) (refl_equal T
43 (TLRef (match (blt (trans p i) n0) with [true \Rightarrow (trans p i) | false
44 \Rightarrow (plus (trans p i) n)]))) (lift1 p (TLRef i)) (H i))))))) hds).
47 \forall (b: B).(\forall (hds: PList).(\forall (u: T).(\forall (t: T).(eq T
48 (lift1 hds (THead (Bind b) u t)) (THead (Bind b) (lift1 hds u) (lift1 (Ss
51 \lambda (b: B).(\lambda (hds: PList).(PList_ind (\lambda (p: PList).(\forall
52 (u: T).(\forall (t: T).(eq T (lift1 p (THead (Bind b) u t)) (THead (Bind b)
53 (lift1 p u) (lift1 (Ss p) t)))))) (\lambda (u: T).(\lambda (t: T).(refl_equal
54 T (THead (Bind b) u t)))) (\lambda (n: nat).(\lambda (n0: nat).(\lambda (p:
55 PList).(\lambda (H: ((\forall (u: T).(\forall (t: T).(eq T (lift1 p (THead
56 (Bind b) u t)) (THead (Bind b) (lift1 p u) (lift1 (Ss p) t))))))).(\lambda
57 (u: T).(\lambda (t: T).(eq_ind_r T (THead (Bind b) (lift1 p u) (lift1 (Ss p)
58 t)) (\lambda (t0: T).(eq T (lift n n0 t0) (THead (Bind b) (lift n n0 (lift1 p
59 u)) (lift n (S n0) (lift1 (Ss p) t))))) (eq_ind_r T (THead (Bind b) (lift n
60 n0 (lift1 p u)) (lift n (S n0) (lift1 (Ss p) t))) (\lambda (t0: T).(eq T t0
61 (THead (Bind b) (lift n n0 (lift1 p u)) (lift n (S n0) (lift1 (Ss p) t)))))
62 (refl_equal T (THead (Bind b) (lift n n0 (lift1 p u)) (lift n (S n0) (lift1
63 (Ss p) t)))) (lift n n0 (THead (Bind b) (lift1 p u) (lift1 (Ss p) t)))
64 (lift_bind b (lift1 p u) (lift1 (Ss p) t) n n0)) (lift1 p (THead (Bind b) u
65 t)) (H u t)))))))) hds)).
68 \forall (f: F).(\forall (hds: PList).(\forall (u: T).(\forall (t: T).(eq T
69 (lift1 hds (THead (Flat f) u t)) (THead (Flat f) (lift1 hds u) (lift1 hds
72 \lambda (f: F).(\lambda (hds: PList).(PList_ind (\lambda (p: PList).(\forall
73 (u: T).(\forall (t: T).(eq T (lift1 p (THead (Flat f) u t)) (THead (Flat f)
74 (lift1 p u) (lift1 p t)))))) (\lambda (u: T).(\lambda (t: T).(refl_equal T
75 (THead (Flat f) u t)))) (\lambda (n: nat).(\lambda (n0: nat).(\lambda (p:
76 PList).(\lambda (H: ((\forall (u: T).(\forall (t: T).(eq T (lift1 p (THead
77 (Flat f) u t)) (THead (Flat f) (lift1 p u) (lift1 p t))))))).(\lambda (u:
78 T).(\lambda (t: T).(eq_ind_r T (THead (Flat f) (lift1 p u) (lift1 p t))
79 (\lambda (t0: T).(eq T (lift n n0 t0) (THead (Flat f) (lift n n0 (lift1 p u))
80 (lift n n0 (lift1 p t))))) (eq_ind_r T (THead (Flat f) (lift n n0 (lift1 p
81 u)) (lift n n0 (lift1 p t))) (\lambda (t0: T).(eq T t0 (THead (Flat f) (lift
82 n n0 (lift1 p u)) (lift n n0 (lift1 p t))))) (refl_equal T (THead (Flat f)
83 (lift n n0 (lift1 p u)) (lift n n0 (lift1 p t)))) (lift n n0 (THead (Flat f)
84 (lift1 p u) (lift1 p t))) (lift_flat f (lift1 p u) (lift1 p t) n n0)) (lift1
85 p (THead (Flat f) u t)) (H u t)))))))) hds)).
87 theorem lift1_cons_tail:
88 \forall (t: T).(\forall (h: nat).(\forall (d: nat).(\forall (hds: PList).(eq
89 T (lift1 (PConsTail hds h d) t) (lift1 hds (lift h d t))))))
91 \lambda (t: T).(\lambda (h: nat).(\lambda (d: nat).(\lambda (hds:
92 PList).(PList_ind (\lambda (p: PList).(eq T (lift1 (PConsTail p h d) t)
93 (lift1 p (lift h d t)))) (refl_equal T (lift h d t)) (\lambda (n:
94 nat).(\lambda (n0: nat).(\lambda (p: PList).(\lambda (H: (eq T (lift1
95 (PConsTail p h d) t) (lift1 p (lift h d t)))).(eq_ind_r T (lift1 p (lift h d
96 t)) (\lambda (t0: T).(eq T (lift n n0 t0) (lift n n0 (lift1 p (lift h d
97 t))))) (refl_equal T (lift n n0 (lift1 p (lift h d t)))) (lift1 (PConsTail p
98 h d) t) H))))) hds)))).
101 \forall (f: F).(\forall (hds: PList).(\forall (t: T).(\forall (ts:
102 TList).(eq T (lift1 hds (THeads (Flat f) ts t)) (THeads (Flat f) (lifts1 hds
103 ts) (lift1 hds t))))))
105 \lambda (f: F).(\lambda (hds: PList).(\lambda (t: T).(\lambda (ts:
106 TList).(TList_ind (\lambda (t0: TList).(eq T (lift1 hds (THeads (Flat f) t0
107 t)) (THeads (Flat f) (lifts1 hds t0) (lift1 hds t)))) (refl_equal T (lift1
108 hds t)) (\lambda (t0: T).(\lambda (t1: TList).(\lambda (H: (eq T (lift1 hds
109 (THeads (Flat f) t1 t)) (THeads (Flat f) (lifts1 hds t1) (lift1 hds
110 t)))).(eq_ind_r T (THead (Flat f) (lift1 hds t0) (lift1 hds (THeads (Flat f)
111 t1 t))) (\lambda (t2: T).(eq T t2 (THead (Flat f) (lift1 hds t0) (THeads
112 (Flat f) (lifts1 hds t1) (lift1 hds t))))) (eq_ind_r T (THeads (Flat f)
113 (lifts1 hds t1) (lift1 hds t)) (\lambda (t2: T).(eq T (THead (Flat f) (lift1
114 hds t0) t2) (THead (Flat f) (lift1 hds t0) (THeads (Flat f) (lifts1 hds t1)
115 (lift1 hds t))))) (refl_equal T (THead (Flat f) (lift1 hds t0) (THeads (Flat
116 f) (lifts1 hds t1) (lift1 hds t)))) (lift1 hds (THeads (Flat f) t1 t)) H)
117 (lift1 hds (THead (Flat f) t0 (THeads (Flat f) t1 t))) (lift1_flat f hds t0
118 (THeads (Flat f) t1 t)))))) ts)))).
121 \forall (ts: TList).(eq TList (lifts1 PNil ts) ts)
123 \lambda (ts: TList).(TList_ind (\lambda (t: TList).(eq TList (lifts1 PNil t)
124 t)) (refl_equal TList TNil) (\lambda (t: T).(\lambda (t0: TList).(\lambda (H:
125 (eq TList (lifts1 PNil t0) t0)).(eq_ind_r TList t0 (\lambda (t1: TList).(eq
126 TList (TCons t t1) (TCons t t0))) (refl_equal TList (TCons t t0)) (lifts1
130 \forall (h: nat).(\forall (d: nat).(\forall (hds: PList).(\forall (ts:
131 TList).(eq TList (lifts1 (PCons h d hds) ts) (lifts h d (lifts1 hds ts))))))
133 \lambda (h: nat).(\lambda (d: nat).(\lambda (hds: PList).(\lambda (ts:
134 TList).(TList_ind (\lambda (t: TList).(eq TList (lifts1 (PCons h d hds) t)
135 (lifts h d (lifts1 hds t)))) (refl_equal TList TNil) (\lambda (t: T).(\lambda
136 (t0: TList).(\lambda (H: (eq TList (lifts1 (PCons h d hds) t0) (lifts h d
137 (lifts1 hds t0)))).(eq_ind_r TList (lifts h d (lifts1 hds t0)) (\lambda (t1:
138 TList).(eq TList (TCons (lift h d (lift1 hds t)) t1) (TCons (lift h d (lift1
139 hds t)) (lifts h d (lifts1 hds t0))))) (refl_equal TList (TCons (lift h d
140 (lift1 hds t)) (lifts h d (lifts1 hds t0)))) (lifts1 (PCons h d hds) t0)