(* RELOCATION ***************************************************************)
-(* Policy: depth (level) metavariables: d, e
- height metavariables : h, k
+(* Policy: level metavariables : d, e
+ height metavariables: h, k
*)
(* Note: indexes start at zero *)
let rec lift h d M on M ≝ match M with
#d #h #i #H elim (le_to_or_lt_eq … H) -H
normalize // /3 width=1/
qed.
-
+(*
lemma lift_vref_pred: ∀d,i. d < i → ↑[d, 1] #(i-1) = #i.
#d #i #Hdi >lift_vref_ge /2 width=1/
<plus_minus_m_m // /2 width=2/
qed.
-
+*)
lemma lift_id: ∀M,d. ↑[d, 0] M = M.
#M elim M -M
[ #i #d elim (lt_or_ge i d) /2 width=1/
lemma lstar_liftable: ∀T,R. (∀t. liftable (R t)) →
∀l. liftable (lstar T … R l).
-#T #R #HR #l #h #M1 #M2 #H elim H -l -M1 -M2 // /3 width=3/
+#T #R #HR #l #h #M1 #M2 #H
+@(lstar_ind_l ????????? H) -l -M1 // /3 width=3/
qed.
lemma lstar_deliftable_sn: ∀T,R. (∀t. deliftable_sn (R t)) →
∀l. deliftable_sn (lstar T … R l).
-#T #R #HR #l #h #N1 #N2 #H elim H -l -N1 -N2 /2 width=3/
-#t #N1 #N #HN1 #l #N2 #_ #IHN2 #d #M1 #HMN1
+#T #R #HR #l #h #N1 #N2 #H
+@(lstar_ind_l ????????? H) -l -N1 /2 width=3/
+#t #l #N1 #N #HN1 #_ #IHN2 #d #M1 #HMN1
elim (HR … HN1 … HMN1) -N1 #M #HM1 #HMN
elim (IHN2 … HMN) -N /3 width=3/
qed-.