proposition: Lemma θ0_preserves_bind A B (c1 c2 : MFreePr A) (f1 f2 : A -> MFreePr B) (Hc : θ0 c1 = θ0 c2) (Hf : forall v, θ0 (f1 v) = θ0 (f2 v)) : θ0 (bindrFree _ _ c1 f1) = θ0 (bindrFree _ _ c2 f2).
proof: Proof. pose (rmm_law2 _ _ _ _ (@unary_theta_dens) _ _ f1). simpl in e. apply equal_f with (x := c1) in e. rewrite /θ0 /unary_theta_dens /=. rewrite e. pose (rmm_law2 _ _ _ _ (@unary_theta_dens) _ _ f2). simpl in e0. apply equal_f with (x := c2) in e0. rewrite /θ0 /unary_theta_dens /=. rewrite e0. rewrite /θ0 /unary_theta_dens /= in Hc. rewrite Hc. rewrite /θ0 /unary_theta_dens /= in Hf. f_equal. extensionality x. apply Hf. Qed.
imports: Coq(RelationClasses Morphisms Utf8) Mon(FiniteProbabilities SPropMonadicStructures SpecificationMonads MonadExamples SPropBase) Relational(OrderEnrichedCategory OrderEnrichedRelativeMonadExamples Commutativity GenericRulesSimple) mathcomp(all_ssreflect all_algebra reals distr realsum) Crypt(Axioms ChoiceAsOrd SubDistr Couplings Theta_dens Theta_exCP LaxComp FreeProbProg RelativeMonadMorph_prod)