proposition: Lemma tree_map_pred_succ_4 : forall t, tree_map pred (tree_map S t) = t.
proof: Proof. Proof using. intros. induction_wf IH: subtree_wf t. destruct t as [|ts]; simpl. fequals. fequals. induction ts; simpl. fequals. fequals. applys IH. auto. applys IHts. introv M. inverts M. auto. Qed.
imports: TLC(LibTactics) TLC(LibLogic LibEqual LibList LibRelation LibWf LibList LibLN)