proposition: Lemma valid_package_cons : ∀ L I i A B f E p, ValidPackage L I (fset E) (mkfmap p) → (∀ x, ValidCode L I (f x)) → i \notin (λ '(i,_), i) @: fset E → ValidPackage L I (fset ((i, (A, B)) :: E)) (mkfmap ((i, mkdef A B f) :: p)).
proof: Proof. intros L I i A B f E p hp hf hi. apply prove_valid_package. intros o ho. rewrite in_fset in ho. rewrite in_cons in ho. move: ho => /orP [ho | ho]. - move: ho => /eqP ho. subst o. rewrite mkfmapE. cbn. exists f. destruct (eqn i i) eqn:e. 2:{ move: e => /eqP. contradiction. } intuition auto. - rewrite -in_fset in ho. eapply from_valid_package in hp. specialize (hp _ ho). destruct o as [id [S T]]. destruct hp as [g [eg hg]]. rewrite mkfmapE. cbn. destruct (eqn id i) eqn:e. 1:{ move: e => /eqP e. subst id. eapply mem_imfset with (f := λ '(i,_), i) in ho. unfold "\notin" in hi. rewrite ho in hi. discriminate. } rewrite mkfmapE in eg. exists g. 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)