proposition: Lemma union_spec' s1 s2 x : InT x (union s1 s2) <-> InT x s1 \/ InT x s2.
proof: Proof. unfold union. destruct compare_height. - apply linear_union_spec. - apply fold_add_spec. - rewrite fold_add_spec. tauto. Qed.
imports: Bool List BinPos Pnat Setoid SetoidList PeanoNat