proposition: Lemma subs_cons x (xs : seq A) : subs (x :: xs) = let t' := subs xs in fmap (cons x) t' [~] t'.
proof: Proof. by []. Qed.
imports: mathcomp(all_ssreflect) imonae_lib HB(structures) ihierarchy imonad_lib Equations(Equations)