proposition: Lemma test_canonical (M : nondetMonad) A (a : M A) (b : A -> M A) : a [~] (fail >>= b) = a [~] fail.
proof: Proof. Set Printing All. Unset Printing All. by rewrite bindfailf. Abort. Section insert_plusMonad. Variable M : plusMonad. Lemma insertC (A : UU0) a b (s : seq A) : (do x <- insert b s; insert a x = do x <- insert a s; insert b x :> M _)%Do. Proof. have [n ns] := ubnP (size s); elim: n s ns a b => // n ih s ns a b. case: s ns => [|h t]. by rewrite !insertE !bindretf !insertE altC !fmapE !bindretf. rewrite ltnS /= => ns. rewrite (insertE _ (h :: t)) alt_bindDl bindretf. rewrite [in LHS](insertE _ [:: b, h & t]) [in LHS](insertE _ (h :: t)). rewrite [in RHS](insertE _ (h :: t)) [in RHS]alt_bindDl bindretf. rewrite 2![in RHS]insertE. rewrite [in LHS]alt_fmapDr ![in LHS]altA [in LHS](altC (Ret [:: a, b, h & t])). rewrite -!altA; congr (_ [~] _); first by rewrite fmapE bindretf. rewrite alt_fmapDr -!altA; congr (_ [~] _); first by rewrite fmapE bindretf. rewrite [in LHS]altC bind_fmap /= [in LHS]/comp /=. under eq_bind do rewrite insertE. rewrite alt_bindDr. under [in X in (_ [~] X) [~] _]eq_bind do rewrite fmapE. rewrite -bindA [in LHS]ih // [in RHS]altC bind_fmap /= [in RHS]/comp /=. under [in RHS]eq_bind do rewrite insertE. rewrite alt_bindDr [in RHS]altC -!altA; congr (_ [~] _). rewrite !fmapE !bindA. by under [in RHS]eq_bind do rewrite !bindretf. rewrite [in RHS]altC; congr (_ [~] _); last first. rewrite !fmapE !bindA. by under eq_bind do rewrite bindretf. rewrite bindA. by under [in RHS]eq_bind do rewrite fmapE. Qed.
imports: mathcomp(all_ssreflect) imonae_lib HB(structures) ihierarchy imonad_lib Equations(Equations)