proposition: Lemma subset_snoc_l : forall T x, forall l1 l2 : list T, (forall y, LIn y l1 -> y = x) -> subset l1 (snoc l2 x).
proof: Proof. unfold subset; sp. apply in_snoc. apply_in_hyp p; sp. Qed.
imports: UsefulTypes bin_rels Omega