fact: Fixpoint joinRose {A : Type} (r : Rose (Rose A)) : Rose A := match r with | MkRose (MkRose a ts) tts => MkRose a (lazy ((List.map joinRose (force tts)) ++ (force ts))) end.
imports: List mathcomp.ssreflect.ssreflect