proposition: Lemma insertE (a : A) s : insert a s = if s isn't h :: t then Ret [:: a] else Ret (a :: h :: t) [~] fmap (cons h) (insert a t).
proof: Proof. by case: s. Qed.
imports: mathcomp(all_ssreflect) imonae_lib HB(structures) ihierarchy imonad_lib Equations(Equations)