proposition: Lemma parable_trim : ∀ E1 E2 p1 p2, fdisjoint (idents E1) (idents E2) → Parable (trim E1 p1) (trim E2 p2).
proof: Proof. intros E1 E2 p1 p2 h. unfold Parable. eapply fdisjoint_trans. { eapply domm_trim. } rewrite fdisjointC. eapply fdisjoint_trans. { eapply domm_trim. } rewrite fdisjointC. auto. 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)