Commit b70f1bcb authored by Joseph Tassarotti's avatar Joseph Tassarotti

Revert spurious change to ref file.

parent dfefb918
...@@ -118,7 +118,7 @@ Tactic failure: iSpecialize: cannot instantiate (⌜φ⌝ → P -∗ False)%I wi ...@@ -118,7 +118,7 @@ Tactic failure: iSpecialize: cannot instantiate (⌜φ⌝ → P -∗ False)%I wi
============================ ============================
"H1" : ⌜S (S (S x)) = y⌝ "H1" : ⌜S (S (S x)) = y⌝
--------------------------------------□ --------------------------------------□
"H2" : ⌜1 + y = z⌝ "H2" : ⌜(1 + y)%nat = z⌝
--------------------------------------∗ --------------------------------------∗
⌜S (S (S x)) = y⌝ ⌜S (S (S x)) = y⌝
......
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