(* RELOCATION MAP ***********************************************************)
-lemma pn_split: â\88\80f. (â\88\83g. â\86\91g = f) â\88¨ (â\88\83g. ⫯g = f).
+lemma pn_split: â\88\80f. (â\88\83g. ⫯g = f) â\88¨ (â\88\83g. â\86\91g = f).
@case_prop /3 width=2 by or_introl, or_intror, ex_intro/
qed-.