proposition: Lemma part_function_inv_strext : forall x y (Hx : P x) (Hy : P y), [--] (F x Hx) [#] [--] (F y Hy) -> x [#] y.
proof: Proof. intros x y Hx Hy H. apply pfstrx with F Hx Hy. apply un_op_strext_unfolded with (cg_inv (c:=G)); assumption. Qed.
imports: CoRN.tactics.CornTac CoRN.algebra.CMonoids