proposition: Lemma in_fsubset : ∀ {e} {S1 S2 : Interface}, fsubset S1 S2 → e \in S1 → e \in S2.
proof: Proof. intros e S1 S2 hs h. unfold fsubset in hs. move: hs. move /eqP => hs. rewrite -hs. rewrite in_fsetU. apply/orP. auto. 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)