(* *)
(**************************************************************************)
-include "ground_2/relocation/rtmap_basic.ma".
+include "ground/relocation/rtmap_basic.ma".
include "static_2/relocation/lifts.ma".
include "apps_2/models/veq.ma".
qed-.
lemma lifts_SO_fwd_vpush (M) (gv): is_model M → is_extensional M →
- ∀T1,T2. ⇧*[1] T1 ≘ T2 →
+ ∀T1,T2. ⇧[1] T1 ≘ T2 →
∀lv,d. ⟦T1⟧[gv,lv] ≗{M} ⟦T2⟧[gv,⫯[0←d]lv].
/2 width=3 by lifts_fwd_vpush_aux/ qed-.