Commit 605562ba authored by Jonas Kastberg Hinrichsen's avatar Jonas Kastberg Hinrichsen
Browse files

Test

parent 77eb6feb
......@@ -111,7 +111,7 @@ Lemma stype_map_ext {A} {B : ofeT} (f g : A → B) (st : stype A) :
( x, f x g x) stype_map f st stype_map g st.
Proof.
intros Hf. induction st; simpl.
Admitted.
Admitted.
Instance styope_map_ne {A B : ofeT} (f : A B) n:
Proper (dist n ==> dist n) f Proper (dist n ==> dist n) (stype_map f).
Proof.
......
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