proposition: Lemma valid_package1 : ∀ L I i A B f, (∀ x, ValidCode L I (f x)) → ValidPackage L I (fset [:: (i, (A, B))]) (mkfmap [:: (i, mkdef A B f)]).
proof: Proof. intros L I i A B f hf. apply prove_valid_package. intros o ho. rewrite in_fset in ho. rewrite mem_seq1 in ho. move: ho => /eqP ho. subst o. cbn. exists f. destruct (eqn i i) eqn:e. 2:{ move: e => /eqP. contradiction. } intuition 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)