proposition: Lemma present_balance2 : forall n (a : rtree n) (y : nat) c2 (b : rbtree c2 n), present z (pr2 (balance2 a y b)) <-> rpresent z a \/ z = y \/ present z b.
proof: Proof. intros. funelim (balance2 a y b); subst; simpl in *; tauto. Qed.
imports: Bool Arith List Program Equations(Equations) Wellfounded Arith Lia