proposition: Lemma trimmed_package_cons : ∀ i A B f p E, trimmed (fset E) (mkfmap p) → trimmed (fset ((i, (A, B)) :: E)) (mkfmap ((i, mkdef A B f) :: p)).
proof: Proof. intros i A B f p E h. unfold trimmed. unfold trim. apply eq_fmap. intro n. rewrite filtermE. rewrite mkfmapE. simpl. destruct (n == i) eqn:e. - simpl. move: e => /eqP e. subst. rewrite in_fset. rewrite in_cons. rewrite eqxx. simpl. reflexivity. - unfold trimmed, trim in h. apply eq_fmap in h. specialize (h n). rewrite filtermE in h. rewrite mkfmapE in h. rewrite -[X in _ = X]h. destruct (getm_def p n) as [[S [T g]]|] eqn:e'. 2:{ rewrite e'. reflexivity. } rewrite e'. simpl. rewrite !in_fset. rewrite in_cons. destruct ((n, (S, T)) == (i, (A, B))) eqn:e2. 1:{ exfalso. move: e2 => /eqP e2. noconf e2. rewrite eqxx in e. discriminate. } rewrite e2. simpl. reflexivity. 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)