Commit 0a5ee4f4 authored by Robbert Krebbers's avatar Robbert Krebbers

Version of fresh using an existential.

parent 87d19f4f
......@@ -807,6 +807,8 @@ Section fresh.
apply IH. by rewrite E.
Qed.
Lemma exist_fresh X : x, x X.
Proof. exists (fresh X). apply is_fresh. Qed.
Lemma Forall_fresh_NoDup X xs : Forall_fresh X xs NoDup xs.
Proof. induction 1; by constructor. Qed.
Lemma Forall_fresh_elem_of X xs x : Forall_fresh X xs x xs x X.
......
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