proposition: Lemma releffobs_eq_effobs2 : forall A1 A2 c1 c2, θapp A1 A2 ⟨c1, c2⟩ = bind (θ2 A2 c2) (fun b : A2 => bind (θ1 A1 c1) (fun a : A1 => ret ⟨ a, b ⟩)).
proof: Proof. move=> A1 A2 //= c1 c2. rewrite <- (monad_law2 c2) at 1. rewrite <- (monad_law1 tt (fun _ => c1)) at 1. rewrite θbind /=. rewrite bind_comm. congr bind. extensionality a. destruct a as [[] a2]. rewrite bind_comm //=. rewrite <- (monad_law2 c1) at 1. rewrite <- (monad_law1 tt (fun _ => monad_ret M2 a2)). rewrite θbind. congr bind. extensionality b. destruct b as [a1 []]. apply θret. Qed.
imports: Coq(ssreflect ssrfun ssrbool) Coq(Relation_Definitions Morphisms) Mon(SPropBase SPropMonadicStructures MonadExamples SpecificationMonads DijkstraMonadExamples) Relational(OrderEnrichedCategory OrderEnrichedRelativeMonadExamples)