Commit 8b9a96ad authored by Robbert Krebbers's avatar Robbert Krebbers

Relate "elements" of a finite set to nil.

parent 65171af2
...@@ -38,6 +38,17 @@ Proof. ...@@ -38,6 +38,17 @@ Proof.
apply elem_of_nil_inv; intros x. apply elem_of_nil_inv; intros x.
rewrite elem_of_elements, elem_of_empty; tauto. rewrite elem_of_elements, elem_of_empty; tauto.
Qed. Qed.
Lemma elements_empty_inv X : elements X = [] X .
Proof.
intros HX; apply elem_of_equiv_empty; intros x.
rewrite <-elem_of_elements, HX, elem_of_nil. tauto.
Qed.
Lemma elements_empty' X : elements X = [] X .
Proof.
split; intros HX; [by apply elements_empty_inv|].
by rewrite <-Permutation_nil, HX, elements_empty.
Qed.
Lemma elements_union_singleton (X : C) x : Lemma elements_union_singleton (X : C) x :
x X elements ({[ x ]} X) x :: elements X. x X elements ({[ x ]} X) x :: elements X.
Proof. Proof.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment