proposition: Lemma refin_ret_insert (M : altCIMonad) (A : UU0) h (t : seq A) : Ret (h :: t) `<=` (insert h t : M _).
proof: Proof. elim: t h => [h|t1 t2 ih h]; first by rewrite insertE; exact: refin_refl. by rewrite insertE; exact: refinR. Qed.
imports: mathcomp(all_ssreflect) imonae_lib HB(structures) ihierarchy imonad_lib Equations(Equations)