proposition: Lemma valid_scheme : ∀ A L I c, @ValidCode fset0 [interface] A c → ValidCode L I c.
proof: Proof. intros A L I c h. eapply valid_injectMap. 2: eapply valid_injectLocations. 1-2: eapply fsub0set. rewrite -fset0E in h. auto. Qed.
imports: mathcomp(ssreflect ssrbool ssrnat eqtype seq eqtype choice) extructures(ord fset fmap) Crypt(Prelude pkg_core_definition pkg_composition pkg_notation choice_type RulesStateProb) Coq(Utf8 FunctionalExtensionality Setoids.Setoid Classes.Morphisms) Equations(Equations)