proposition: Lemma trimmed_empty_package : trimmed [interface] (mkfmap nil).
proof: Proof. unfold trimmed. simpl. unfold trim. apply eq_fmap. intro n. rewrite filtermE. rewrite emptymE. 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)