fact: Fixpoint ltree_to_ntree {A : Type} (t : ltree A) {struct t} : ntree A := match t with | lnode _ x l => nnode A x ((fix list_tree_to_nforest (l' : list (ltree A)) : nforest A := match l' with nil => nnil A | t1 :: tl => ncons A (ltree_to_ntree t1) (list_tree_to_nforest tl) end) l) end.
imports: List