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