(* Properties with extensional equivalence **********************************)
-lemma mf_gc_id: â\88\80j. â\87¡[j]mf_gi â\89\90 mf_gi.
+lemma mf_gc_id: â\88\80j. â\87¡[j]mf_gi â\8a\9c mf_gi.
// qed.
lemma mf_vlift_comp (l): compatible_2 … (mf_vlift l) (exteq …) (exteq …).
(* Main properties with extensional equivalence *****************************)
-theorem mf_vlift_swap: â\88\80l1,l2. l2 â\89¤ l1 â\86\92 â\88\80v. â\87¡[l2]â\87¡[l1]v â\89\90 ⇡[↑l1]⇡[l2]v.
+theorem mf_vlift_swap: â\88\80l1,l2. l2 â\89¤ l1 â\86\92 â\88\80v. â\87¡[l2]â\87¡[l1]v â\8a\9c ⇡[↑l1]⇡[l2]v.
/2 width=1 by flifts_basic_swap/ qed-.