proposition: Theorem present_insert_Black : forall n (t : rbtree Black n), present z (pr2 (insert t)) <-> (z = x \/ present z t).
proof: Proof. present_insert t t. Qed.
imports: Bool Arith List Program Equations(Equations) Wellfounded Arith Lia