proposition: Lemma valid_empty_package : ∀ L I, ValidPackage L I [interface] emptym.
proof: Proof. intros L I. rewrite -fset0E. apply prove_valid_package. intros [id [S T]] ho. eapply fromEmpty. 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)