Commit 81b17d8c authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Remove unused premise of iso_cofe_subtype.

parent 1c14ae6f
......@@ -1147,7 +1147,6 @@ Qed.
Section iso_cofe_subtype.
Context {A B : ofeT} `{Cofe A} (P : A Prop) (f : x, P x B) (g : B A).
Context (Pg : y, P (g y)).
Context (g_dist : n y1 y2, y1 {n} y2 g y1 {n} g y2).
Let Hgne : NonExpansive g.
Proof. intros n y1 y2. apply g_dist. Qed.
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