#g #H elim (pn_split g) * #f #Hf
/4 width=3 by isuni_inv_next, isuni_inv_push, or_introl, or_intror, ex2_intro/
qed-.
(* basic forward lemmas *****************************************************)
#g #H elim (pn_split g) * #f #Hf
/4 width=3 by isuni_inv_next, isuni_inv_push, or_introl, or_intror, ex2_intro/
qed-.
(* basic forward lemmas *****************************************************)