Commit 79da67c9 authored by Daniël Louwrink's avatar Daniël Louwrink

fix pair example

parent 76e934c0
Pipeline #27734 passed with stage
in 5 minutes and 45 seconds
......@@ -11,6 +11,8 @@ Section pair.
Proof.
rewrite /prog.
iApply ltyped_lam. iApply ltyped_pair.
iApply ltyped_recv. iApply ltyped_recv.
iApply ltyped_recv.
2:{ iApply ltyped_recv. by rewrite /binder_insert lookup_insert. }
by rewrite lookup_insert.
Qed.
End pair.
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