(* *)
(**************************************************************************)
-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".
(* Forward lemmas with generic relocation ***********************************)
fact lifts_fwd_vpush_aux (M): is_model M → is_extensional M →
- â\88\80f,T1,T2. â\87§*[f] T1 â\89\98 T2 â\86\92 â\88\80m. ð\9d\90\81❨m,1❩ = f →
+ â\88\80f,T1,T2. â\87§*[f] T1 â\89\98 T2 â\86\92 â\88\80m. ð\9d\90\9b❨m,1❩ = f →
∀gv,lv,d. ⟦T1⟧[gv,lv] ≗{M} ⟦T2⟧[gv,⫯[m←d]lv].
#M #H1M #H2M #f #T1 #T2 #H elim H -f -T1 -T2
[ #f #s #m #Hf #gv #lv #d