parent 556a5992
......@@ -401,7 +401,7 @@ Section infinite.
(** Properties about the [fresh] operation on finite sets *)
Global Instance fresh_proper: Proper ((@{C}) ==> (=)) fresh.
Proof. unfold fresh, set_fresh. solve_proper. Qed.
Proof. unfold fresh, set_fresh. Morphisms.solve_proper. Qed.
Lemma is_fresh X : fresh 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