Commit 652aebfc authored by Ralf Jung's avatar Ralf Jung
Browse files

show that dist_later is a subrelation of dist

parent 15be3526
......@@ -189,6 +189,9 @@ Arguments dist_later _ !_ _ _ /.
Global Instance dist_later_equivalence A n : Equivalence (@dist_later A n).
Proof. destruct n as [|n]. by split. apply dist_equivalence. Qed.
Lemma dist_dist_later {A : ofeT} n (x y : A) : dist n x y dist_later n x y.
Proof. intros Heq. destruct n; first done. exact: dist_S. Qed.
Notation Contractive f := ( n, Proper (dist_later n ==> dist n) f).
Instance const_contractive {A B : ofeT} (x : A) : Contractive (@const A B x).
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