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

prepare for weaker f_equiv

parent 6edcd231
No related branches found
No related tags found
No related merge requests found
Pipeline #54467 passed
Hide whitespace changes
Inline Side-by-side
Showing
with 1 addition and 1 deletion
theories/typing/own.v
+ 1
− 1
View file @ 8d7575d0
...@@ -38,7 +38,7 @@ Section own. ...@@ -38,7 +38,7 @@ Section own.
- by rewrite left_id shift_loc_0. - by rewrite left_id shift_loc_0.
- by rewrite right_id Nat.add_0_r. - by rewrite right_id Nat.add_0_r.
- iSplit. by iIntros "[[]?]". by iIntros "[]". - iSplit. by iIntros "[[]?]". by iIntros "[]".
- rewrite hist_freeable_op_eq. f_equiv. - rewrite hist_freeable_op_eq. f_equiv; [|done..].
by rewrite -Qp_div_add_distr pos_to_Qp_add -Nat2Pos.inj_add. by rewrite -Qp_div_add_distr pos_to_Qp_add -Nat2Pos.inj_add.
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