proposition: Lemma isinj_pr1_PosetEquivalence (X Y : Poset) : isInjective (pr1 : X ≅ Y -> X ≃ Y).
proof: Proof. intros f g. apply isweqonpathsincl. apply isincl_pr1_PosetEquivalence. Defined.
imports: UniMath.Foundations.Propositions