proposition: Theorem ntree_o_ltree {A:Type}: forall t : ltree A, ntree_to_ltree (ltree_to_ntree t) = t.
proof: Proof. intros t; elim t using ltree_ind2 with ( Q := fun l => nforest_to_list_ltree A ((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) = l ). - simpl; intros a l IHl; rewrite IHl; trivial. - simpl; trivial. - simpl; intros t' IHt' tl IHtl; rewrite IHt'; rewrite IHtl; trivial. Qed.
imports: List