Commit 4e7e8579 authored by Robbert Krebbers's avatar Robbert Krebbers

Add lemma Shot_core.

parent f5334942
......@@ -158,6 +158,9 @@ Instance one_shot_op : Op (one_shot A) := λ x y,
Lemma Shot_op a b : Shot a Shot b = Shot (a b).
Proof. done. Qed.
Lemma Shot_core a : core (Shot a) = Shot (core a).
Proof. done. Qed.
Lemma Shot_incl a b : Shot a Shot b a b.
Proof.
split; intros [c H].
......
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