proposition: Lemma injectSubset : ∀ {locs1 locs2 : {fset Location}} {l : Location}, fsubset locs1 locs2 → l \in locs1 → l \in locs2.
proof: Proof. intros locs1 locs2 l Hfsubset H. unfold fsubset in Hfsubset. move: Hfsubset. move /eqP => Q. rewrite -Q. rewrite in_fsetU. apply/orP. by left. Defined.
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)