proposition: Lemma bind_liftM2_size (f : seq A -> seq B -> seq C) (m1 : M (seq A)) (m2 : M (seq B)) n : (forall a b, size (f a b) = size a + size b + n) -> liftM2 f m1 m2 >>= (fun x => Ret (x, size x)) = liftM2 (fun a b => (f a.1 b.1, a.2 + b.2 + n)) (m1 >>= (fun x => Ret (x, size x))) (m2 >>= (fun x => Ret (x, size x))).
proof: Proof. move=> hf. rewrite /liftM2 !bindA; bind_ext => x1. rewrite !bindretf !bindA. bind_ext=> x2. by rewrite !bindretf /= hf. Qed.
imports: ssrmatching mathcomp(all_ssreflect) monae_lib HB(structures) hierarchy