proposition: Lemma tree_map_pred_succ_3 : forall t, tree_map pred (tree_map S t) = t.
proof: Proof. Proof using. intros. induction t using tree_induct_mem; simpl. fequals. fequals. induction ts; simpl. fequals. fequals. apply H. constructor. apply IHts. introv M. apply H. auto. Qed.
imports: TLC(LibTactics) TLC(LibLogic LibEqual LibList LibRelation LibWf LibList LibLN)