Commit 91aede9b authored by Ralf Jung's avatar Ralf Jung
Browse files


parent 6828183c
......@@ -802,7 +802,7 @@ Proof.
apply nsteps_inv_r in Hstps as [[t3 σ3] [Hstps Hρ]]; simpl in *.
destruct (IHn _ _ Hstps) as (t2'&t2''&σ2'&Hostps&?&?&Hprstps); simplify_eq.
edestruct @erased_step_pure_step_tp as [[? Hint]|Hext]; simplify_eq/=;
eauto 10; [|done..].
first apply Hρ; eauto 10; [].
destruct Hext as (i&ei&t2'&efs&e'&κ&Hi1&Ht2&Hpstp);
rewrite /erase_tp list_lookup_fmap in Hi1.
Supports Markdown
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