proposition: Theorem present_ins : forall c n (t : rbtree c n), present_insResult t (ins t).
proof: Proof. intros. funelim (ins t); simp present_insResult in *; simpl in *; try match goal with [ |- context [balance1 ?A ?B ?C] ] => generalize (present_balance1 A B C) end; try match goal with [ |- context [balance2 ?A ?B ?C] ] => generalize (present_balance2 A B C) end; try tauto. Qed.
imports: Bool Arith List Program Equations(Equations) Wellfounded Arith Lia