proposition: Lemma symbols_prop1 : symbols \o const 1 = (M # wrap) \o const fresh :> (A -> M _).
proof: Proof. apply: funext => n. transitivity (@symbols _ M 1) => //. rewrite symbolsE sequence_cons sequence_nil. under eq_bind do rewrite bindretf. by rewrite compE [in RHS]fmapE. Qed.
imports: mathcomp(all_ssreflect) imonae_lib HB(structures) ihierarchy imonad_lib ifail_lib