Commit 94d26232 authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan
Browse files

Apply 1 suggestion(s) to 1 file(s)

parent e15ec18b
......@@ -52,7 +52,7 @@ Definition wp_pre `{!irisG Λ Σ} (s : stuckness)
Local Instance wp_pre_contractive `{!irisG Λ Σ} s : Contractive (wp_pre s).
Proof.
rewrite /wp_pre /==> n wp wp' Hwp E e1 Φ.
rewrite /wp_pre /= => n wp wp' Hwp E e1 Φ.
repeat (f_contractive || f_equiv); apply Hwp.
Qed.
......
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