proposition: Lemma flat_valid_package : ∀ L I E p, ValidPackage L I E p → flat E.
proof: Proof. intros L I E p hp. intros i [u1 u2] [v1 v2] h1 h2. eapply from_valid_package in hp. specialize (hp _ h1) as h1'. specialize (hp _ h2) as h2'. simpl in *. destruct h1' as [f [ef _]]. destruct h2' as [g [eg _]]. rewrite ef in eg. noconf eg. 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)