proposition: Lemma mpair_arbitrary (T : UU0) a (x y : seq T) : 0 < size x -> 0 < size y -> mpair (arbitrary a x, arbitrary a y) = arbitrary (a, a) (cp x y) :> M (T * T)%type.
proof: Proof. elim: x y => // x; case=> [_ y _ size_y|x' xs IH y _ size_y]; apply/esym. exact/mpair_arbitrary_base_case. set xxs := x' :: xs. rewrite /cp -cat1s allpairs_cat -/(cp _ _) cp1 /= arbitrary_cat; last 2 first. by rewrite size_map. by rewrite size_cat size_map addn_gt0 size_y. pose n := size y. pose l := size (cp xxs y). rewrite -IH //. rewrite -/xxs. move: (mpair_arbitrary_base_case a x size_y). rewrite {1}/cp [in X in arbitrary _ X]/= cats0 => ->. rewrite -alt_bindDl. by rewrite -arbitrary_cat. Qed.
imports: mathcomp(all_ssreflect) imonae_lib HB(structures) ihierarchy imonad_lib Equations(Equations)