Commit 634fdbb6 authored by Robbert Krebbers's avatar Robbert Krebbers

Fix typo.

parent 97c4d39f
Pipeline #2913 passed with stage
in 9 minutes and 25 seconds
......@@ -584,7 +584,7 @@ Proof. unseal. by destruct mx. Qed.
(* Functions *)
Lemma cofe_funC_equivI {A B} (f g : A -c> B) : f g x, f x g x.
Proof. by unseal. Qed.
Lemma cofe_moreC_equivI {A B : cofeT} (f g : A -n> B) : f g x, f x g x.
Lemma cofe_morC_equivI {A B : cofeT} (f g : A -n> B) : f g x, f x g x.
Proof. by unseal. Qed.
End primitive.
End uPred_primitive.
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