proposition: Lemma in_deq_t : forall A, forall eq : Deq A, forall x : A, forall l, LIn x l [+] !LIn x l.
proof: Proof. induction l; simpl; sp; try (complete (right; sp)). destruct (eq a x); subst; sp. right; sp. Defined.
imports: UsefulTypes bin_rels Omega