proposition: Lemma linear_inter_spec s1 s2 x `(Ok s1, Ok s2) : InT x (linear_inter s1 s2) <-> InT x s1 /\ InT x s2.
proof: Proof. unfold linear_inter. rewrite !rev_elements_rev, treeify_spec, inter_list_spec by (rewrite rev_involutive; auto_tc). rewrite !InA_rev, InA_nil, !elements_spec1 by auto_tc. tauto. Qed.
imports: Bool List BinPos Pnat Setoid SetoidList PeanoNat