proposition: Lemma dlabels_relabel_never_fails : relabel >=> dlabels = symbols \o @size_Tree Symbol.
proof: Proof. by rewrite dlabels_relabel_is_fold symbols_size_is_fold. Qed.
imports: mathcomp(all_ssreflect) monae_lib hierarchy monad_lib fail_lib state_lib