proposition: Corollary inducedPartialOrder_weq {X Y} (f:X≃Y) (R:hrel Y) (po:isPartialOrder R) : isPartialOrder (λ x x' : X, R (f x) (f x')).
proof: Proof. intros. exact (inducedPartialOrder f (incl_injectivity f (weqproperty f)) R po). Defined.
imports: UniMath.Combinatorics.FiniteSets UniMath.Foundations.UnivalenceAxiom UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.DecidablePropositions