proposition: Lemma symbolsS n : symbols n.+1 = (do x <- fresh ; do xs <- symbols n : M _; Ret (x :: xs))%Do.
proof: Proof. by rewrite symbolsE. Qed.
imports: mathcomp(all_ssreflect) monae_lib HB(structures) hierarchy monad_lib fail_lib