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