proposition: Lemma linear_union_spec s1 s2 x : InT x (linear_union s1 s2) <-> InT x s1 \/ InT x s2.
proof: Proof. unfold linear_union. rewrite treeify_spec, union_list_spec, !rev_elements_rev. rewrite !InA_rev, InA_nil, !elements_spec1 by auto_tc. tauto. Qed.
imports: Bool List BinPos Pnat Setoid SetoidList PeanoNat