proposition: Lemma mpair_arbitrary_base_case (T : UU0) a x (y : seq T) : (0 < size y)%nat -> arbitrary (a, a) (cp [:: x] y) = mpair (arbitrary a [:: x], arbitrary a y) :> M _.
proof: Proof. move=> y0; rewrite cp1. transitivity (arbitrary a y >>= (fun y' => Ret (x, y')) : M _). by rewrite -(compE (arbitrary _)) -(arbitrary_naturality a) // compE fmapE. transitivity (do z <- Ret x; do y' <- arbitrary a y; Ret (z, y') : M _)%Do. by rewrite bindretf. by []. Qed.
imports: mathcomp(all_ssreflect) imonae_lib HB(structures) ihierarchy imonad_lib Equations(Equations)