proposition: Lemma loc_package_ext : ∀ {I E} (p1 p2 : loc_package I E), p1.(locs) = p2.(locs) → p1.(locs_pack).(pack) =1 p2.(locs_pack).(pack) → p1 = p2.
proof: Proof. intros I E p1 p2 e1 e2. destruct p1 as [l1 [p1 h1]], p2 as [l2 [p2 h2]]. apply eq_fmap in e2. cbn in *. subst. f_equal. 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)