Commit 4ad619de authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan

cofe -> ofe

parent 010efcf2
......@@ -588,9 +588,9 @@ Proof.
Qed.
(* Functions *)
Lemma cofe_funC_equivI {A B} (f g : A -c> B) : f g x, f x g x.
Lemma ofe_funC_equivI {A B} (f g : A -c> B) : f g x, f x g x.
Proof. by unseal. Qed.
Lemma cofe_morC_equivI {A B : ofeT} (f g : A -n> B) : f g x, f x g x.
Lemma ofe_morC_equivI {A B : ofeT} (f g : A -n> B) : f g x, f x g x.
Proof. by unseal. Qed.
(* Sig ofes *)
......
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