proposition: Lemma disjoint_snoc_r : forall T, forall l1 l2 : list T, forall x : T, disjoint l1 (snoc l2 x) <=> (disjoint l1 l2 # ! LIn x l1).
proof: Proof. unfold disjoint; sp; split; intros. - sp; apply_in_hyp p; trw_h in_snoc p; trw_h not_over_or p; sp. - sp. allrw in_snoc; sp; subst; sp. apply_in_hyp p; sp. Qed.
imports: UsefulTypes bin_rels Omega