Commit bbc61206 authored by Robbert Krebbers's avatar Robbert Krebbers

Remove useless parentheses.

parent c800ca9c
......@@ -1101,8 +1101,7 @@ Section later.
(* f is contractive iff it can factor into `Next` and a non-expansive function. *)
Lemma contractive_alt {B : ofeT} (f : A B) :
Contractive f g : later A B,
(NonExpansive g) ( x, f x g (Next x)).
Contractive f g : later A B, NonExpansive g x, f x g (Next x).
Proof.
split.
- intros Hf. exists (f later_car); split=> // n x y ?. by f_equiv.
......
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