proposition: Theorem PosetEquivalence_rect (X Y : Poset) (P : X ≅ Y -> UU) : (∏ e : X = Y, P (Poset_univalence_map e)) -> ∏ f, P f.
proof: Proof. intros ih ?. set (p := ih (invmap (Poset_univalence _ _) f)). set (h := homotweqinvweq (Poset_univalence _ _) f). exact (transportf P h p). Defined.
imports: UniMath.Combinatorics.FiniteSets UniMath.Foundations.UnivalenceAxiom UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.DecidablePropositions