Commit c46bb2a0 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Version of fresh using an existential.

parent 89ce6ae2
......@@ -807,6 +807,8 @@ Section fresh.
apply IH. by rewrite E.
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.
Supports Markdown
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