proposition: Lemma valid_injectMap : ∀ {A I1 I2} (v : raw_code A), fsubset I1 I2 → ValidCode Locs I1 v → ValidCode Locs I2 v.
proof: Proof. intros A I1 I2 v h p. induction p. all: try solve [ constructor ; auto ]. constructor. 2: eauto. eapply in_fsubset. 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)