proposition: Lemma valid_ID : ∀ L I, flat I → ValidPackage L I I (ID I).
proof: Proof. intros L I hI. apply prove_valid_package. intros [id [S T]] ho. rewrite IDE. destruct getm_def as [[S' T']|] eqn:e. 2:{ exfalso. eapply in_getm_def_None. 2: eauto. exact ho. } eapply getm_def_in in e as hi. eapply hI in hi. specialize (hi ho). noconf hi. simpl. eexists. split. 1: reflexivity. simpl. intro x. exact _. Qed.
imports: Coq(Utf8) Relational(OrderEnrichedCategory OrderEnrichedRelativeMonadExamples) mathcomp(ssreflect eqtype choice seq ssrfun ssrbool ssrnat) extructures(ord fset fmap) Mon(SPropBase) Crypt(Prelude Axioms ChoiceAsOrd StateTransformingLaxMorph choice_type pkg_core_definition RulesStateProb) Equations(Equations)