proposition: Lemma tree_map_pred_succ_2 : forall t, tree_map pred (tree_map S t) = t.
proof: Proof. Proof using. intros. induction t using tree_induct_forall; simpl. fequals. fequals. induction ts; simpl. auto. inverts H. fequals~. Qed.
imports: TLC(LibTactics) TLC(LibLogic LibEqual LibList LibRelation LibWf LibList LibLN)