proposition: Lemma valid_package_cons_upto : ∀ L I i A B A' B' f E p, ValidPackage L I (fset E) (mkfmap p) → (∀ x, ValidCode L I (f x)) → i \notin (λ '(i,_), i) @: fset E → A = A' → B = B' → ValidPackage L I (fset ((i, (A', B')) :: E)) (mkfmap ((i, mkdef A B f) :: p)).
proof: Proof. intros L I i A B A' B' f E p hp hf hi eA eB. subst. eapply valid_package_cons. all: eauto. 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)