proposition: Lemma inter_spec s1 s2 y `{Ok s1, Ok s2} : InT y (inter s1 s2) <-> InT y s1 /\ InT y s2.
proof: Proof. unfold inter. destruct compare_height. - now apply linear_inter_spec. - rewrite filter_spec, mem_spec by auto_tc; tauto. - rewrite filter_spec, mem_spec by auto_tc; tauto. Qed.
imports: Bool List BinPos Pnat Setoid SetoidList PeanoNat