Skip to content
Snippets Groups Projects
Commit df18abd2 authored by Ralf Jung's avatar Ralf Jung
Browse files

fix typo in unmk_cell

parent 6d40a9e8
No related branches found
No related tags found
No related merge requests found
Pipeline #
Hide whitespace changes
Inline Side-by-side
theories/typing/unsafe/cell.v
+ 1
− 1
View file @ df18abd2
...@@ -67,7 +67,7 @@ Section typing. ...@@ -67,7 +67,7 @@ Section typing.
(* Same for the other direction *) (* Same for the other direction *)
Lemma tctx_unmk_cell E L ty p : Lemma tctx_unmk_cell E L ty p :
tctx_incl E L [p ◁ ty] [p ◁ cell ty]. tctx_incl E L [p ◁ cell ty] [p ◁ ty].
Proof. Proof.
iIntros (???) "#LFT $ $ Hty". rewrite !tctx_interp_singleton /=. done. iIntros (???) "#LFT $ $ Hty". rewrite !tctx_interp_singleton /=. done.
Qed. Qed.
......
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