proposition: Lemma arbitrary_cat (T : UU0) (a : T) s t : let m := size s in let n := size t in 0 < m -> 0 < n -> arbitrary a (s ++ t) = arbitrary a s [~] arbitrary a t :> M _.
proof: Proof. elim: s t => [//|s1 s2 IH]. elim/last_ind => // t1 t2 _ m n m0 n0 //. rewrite cat_cons [in LHS]arbitrary_cons; last first. by rewrite size_cat size_rcons addnS. destruct s2 as [|s2 s3] => //. rewrite IH // altA; congr (_ [~] _). by rewrite [in RHS]arbitrary_cons. Qed.
imports: mathcomp(all_ssreflect) imonae_lib HB(structures) ihierarchy imonad_lib Equations(Equations)