proposition: Lemma package_ext : ∀ {L I E} (p1 p2 : package L I E), p1.(pack) =1 p2.(pack) → p1 = p2.
proof: Proof. intros L I E p1 p2 e. destruct p1 as [p1 h1], p2 as [p2 h2]. apply eq_fmap in e. cbn in *. subst. f_equal. apply proof_irrelevance. Qed.
imports: Coq(Utf8) Relational(OrderEnrichedCategory OrderEnrichedRelativeMonadExamples) mathcomp(ssreflect eqtype choice seq ssrfun ssrbool) extructures(ord fset fmap) Mon(SPropBase) Crypt(Prelude Axioms ChoiceAsOrd RulesStateProb StateTransformingLaxMorph choice_type) Equations.Prop.DepElim Equations(Equations)