Commit b57aa587 authored by Robbert Krebbers's avatar Robbert Krebbers

Use `TCEq` so that TC search can establish non-valueness.

parent 0a2f1938
......@@ -79,8 +79,8 @@ Global Instance wp_proper s E e :
Proof.
by intros Φ Φ' ?; apply equiv_dist=>n; apply wp_ne=>v; apply equiv_dist.
Qed.
Lemma wp_contractive s E e n :
to_val e = None
Global Instance wp_contractive s E e n :
TCEq (to_val e) None
Proper (pointwise_relation _ (dist_later n) ==> dist n) (wp (PROP:=iProp Σ) s E e).
Proof.
intros He Φ Ψ HΦ. rewrite !wp_unfold /wp_pre He.
......
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