Commit a25e7a98 authored by Hai Dang's avatar Hai Dang
Browse files

Fix parse error with From

parent f86fc901
......@@ -2252,7 +2252,7 @@ Proof.
clear -Eqeo1 InMb0. apply Some_inj in Eqeo1 as ->. done.
- apply (stk_base_stack_logview SP _ _ _ _ EqTps Eqeo1 _ _
Eqo1 EqeVob InpsIde). }
(* If (u1, o1) is an exchange pair, we know that o1 = S u1. From
(* If (u1, o1) is an exchange pair, we know that o1 = S u1. With
psIde < o1, we have psIde ≤ u1. But we also have u1 < psIde
==> contradiction *)
assert (Eqo1' := stk_xchg_consec SP _ _ _ _ Eqeu1 Eqeo1 In1).
......
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