proposition: Lemma choose_3': forall s s', Equal s s' -> choose s = choose s'.
proof: Proof. setoid_rewrite equal_spec. induction s as [|l IHl o r IHr]. - intros. symmetry. apply choose_empty. assumption. - destruct s' as [|l' o' r']. + generalize (Node l o r) as s. simpl. intros. apply choose_empty. rewrite <- equal_spec in H. apply eq_sym in H. rewrite equal_spec in H. assumption. + simpl. rewrite <- 2andb_lazy_alt, 2andb_true_iff, eqb_true_iff. intros [[<- Hl] Hr]. rewrite (IHl _ Hl), (IHr _ Hr). reflexivity. Qed.
imports: Bool PeanoNat BinPos OrderedType OrderedTypeEx FSetInterface