proposition: Lemma valid_cmd_injectLocations : ∀ A L1 L2 (v : command A), fsubset L1 L2 → ValidCommand L1 import v → ValidCommand L2 import v.
proof: Proof. intros A L1 L2 v h p. destruct p. all: try solve [ constructor ; eauto ]. - constructor. eapply injectSubset. all: eauto. - constructor. eapply injectSubset. all: eauto. 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)