proposition: Lemma Mon_law_2_aux: forall (A: Type) n (x y: mon A), eta_match n x y -> bisim n (run x) (run y).
proof: Proof. cofix CIH; destruct 1. - destruct m. + rewrite run_Bind_Ret, run_Ret. apply bisim_left. apply bisim_now. + rewrite run_Bind_Later, run_Later. eapply bisim_both. apply CIH. apply eta_match_1. + rewrite run_Bind_Bind. apply bisim_left. apply CIH. apply eta_match_2 with (k := K0 _). - destruct m. + rewrite ! run_Bind_Ret. destruct k; simpl. * eapply bisim_both. apply CIH. apply eta_match_1. * eapply bisim_both. apply CIH. apply eta_match_2. + rewrite ! run_Bind_Later. eapply bisim_both. apply CIH. apply eta_match_2. + rewrite ! run_Bind_Bind. eapply bisim_both. apply CIH. apply (eta_match_2 m (Kbind m0 k)). Qed.
imports: Coq(Arith ZArith Psatz Bool String List) CDF(Sequences IMP)