proposition: Lemma diff_spec s1 s2 y `{Ok s1, Ok s2} : InT y (diff s1 s2) <-> InT y s1 /\ ~InT y s2.
proof: Proof. unfold diff. destruct compare_height. - now apply linear_diff_spec. - rewrite filter_spec, Bool.negb_true_iff, <- Bool.not_true_iff_false, mem_spec; intuition. intros x1 x2 EQ. f_equal. now apply mem_proper. - now apply fold_remove_spec. Qed.
imports: Bool List BinPos Pnat Setoid SetoidList PeanoNat