proposition: Theorem present_insert_Red : forall n (t : rbtree Red n), present z (insert t) <-> (z = x \/ present z t).
proof: Proof. intros. funelim (insert t). generalize (present_ins t). simpl. try rewrite present_insResult_equation_1; try rewrite present_insResult_equation_2. funelim (ins t). intros; assumption. intros; assumption. Qed.
imports: Bool Arith List Program Equations(Equations) Wellfounded Arith Lia