proposition: Lemma all_belongs_single_inv : forall xs y v, length xs = 1 -> xs ⊂ (y ∶ v) -> xs = y :: nil.
proof: Proof. induction xs as [ | x xs IHxs ]; intros y v Hlen Hin; simpl in *; auto; inversion Hlen as [ Hlen2 ]. assert (xs = nil) as Hxsnil by (induction xs; simpl in *; auto; inversion Hlen2). rewrite Hxsnil; f_equal. unfold all_belongs in Hin; simpl in Hin. assert (x ∈ (y ∶ v)) as Hin2 by (apply Hin; left; auto). inversion Hin2 as [ | Hfalse ]; auto. inversion Hfalse. Qed.
imports: Utf8 Equalities