proposition: Lemma all_belongs_empty : forall xs, xs ⊂ (@empty A) -> xs = nil.
proof: Proof. induction xs as [ | x ]; intro Hin; simpl in *; auto. unfold all_belongs, belongs in Hin. rewrite dom_empty in Hin. simpl in Hin. elim Hin with x. left; auto. Qed.
imports: Utf8 Equalities