proposition: Theorem ltree_o_ntree {A:Type}: forall t : ntree A, ltree_to_ntree (ntree_to_ltree t) = t.
proof: Proof. intros t; elim t using ntree_ind2 with ( P0 := fun l => (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) (nforest_to_list_ltree _ l) = l ). - simpl; intros a f IHf; rewrite IHf; trivial. - simpl; trivial. - simpl; intros n IHn f IHf; rewrite IHn; rewrite IHf; trivial. Qed.
imports: List