proposition: Lemma in_snoc : forall T, forall l : list T, forall x y : T, LIn x (snoc l y) <=> (LIn x l [+] x = y).
proof: Proof. induction l; simpl; sp. split; sp. trw IHl. apply sum_assoc. Qed.
imports: UsefulTypes bin_rels Omega