proposition: Lemma redo_rev_tree_invol {T} (t : btree T) : redo_rev_tree (redo_rev_tree t) = t.
proof: Proof. funelim (redo_rev_tree t). reflexivity. simp redo_rev_tree. rewrite H, H0. reflexivity. Qed.
imports: Arith Equations(Equations)