proposition: Lemma arbitrary_cons (T : UU0) (def : T) h t : 0 < size t -> arbitrary def (h :: t) = Ret h [~] arbitrary def t :> M _.
proof: Proof. move: def h; elim: t => // a [//|b [|c t]] ih def h _. - by rewrite arbitrary2. - by rewrite /arbitrary /= altA altC (altC (Ret b)). - move: (ih a h erefl); rewrite /arbitrary /= => ->. move: (ih h a erefl); rewrite /arbitrary /= => ->. by rewrite altCA. Qed.
imports: mathcomp(all_ssreflect) imonae_lib HB(structures) ihierarchy imonad_lib Equations(Equations)