'RLiftStar f T1 T2 = (lifts f T1 T2).
definition liftable2_sn: predicate (relation term) ≝
- λR. ∀T1,T2. R T1 T2 → ∀f,U1. ⇧*[f] T1 ≘ U1 →
+ λR. ∀T1,T2. R T1 T2 → ∀f,U1. ⇧*[f] T1 ≘ U1 →
∃∃U2. ⇧*[f] T2 ≘ U2 & R U1 U2.
definition deliftable2_sn: predicate (relation term) ≝
∃∃T2. ⇧*[f] T2 ≘ U2 & R T1 T2.
definition liftable2_bi: predicate (relation term) ≝
- λR. ∀T1,T2. R T1 T2 → ∀f,U1. ⇧*[f] T1 ≘ U1 →
+ λR. ∀T1,T2. R T1 T2 → ∀f,U1. ⇧*[f] T1 ≘ U1 →
∀U2. ⇧*[f] T2 ≘ U2 → R U1 U2.
definition deliftable2_bi: predicate (relation term) ≝
]
qed-.
+lemma lifts_inv_push_zero_sn (f):
+ ∀X. ⇧*[⫯f]#0 ≘ X → #0 = X.
+#f #X #H
+elim (lifts_inv_lref1 … H) -H #i #Hi #H destruct
+lapply (at_inv_ppx … Hi ???) -Hi //
+qed-.
+
+lemma lifts_inv_push_succ_sn (f) (i1):
+ ∀X. ⇧*[⫯f]#(↑i1) ≘ X →
+ ∃∃i2. ⇧*[f]#i1 ≘ #i2 & #(↑i2) = X.
+#f #i1 #X #H
+elim (lifts_inv_lref1 … H) -H #j #Hij #H destruct
+elim (at_inv_npx … Hij) -Hij [|*: // ] #i2 #Hi12 #H destruct
+/3 width=3 by lifts_lref, ex2_intro/
+qed-.
+
(* Inversion lemmas with uniform relocations ********************************)
lemma lifts_inv_lref1_uni: ∀l,Y,i. ⇧*[l] #i ≘ Y → Y = #(l+i).
lift_lref_ge_minus lift_lref_ge_minus_eq
*)
(* Basic_1: removed theorems 8:
- lift_lref_gt
- lift_head lift_gen_head
+ lift_lref_gt
+ lift_head lift_gen_head
lift_weight_map lift_weight lift_weight_add lift_weight_add_O
lift_tlt_dx
*)