Commit 411ccd95 authored by charguer's avatar charguer
Browse files

fix

parent 3bc99621
......@@ -622,7 +622,7 @@ Proof using.
{ unfold hinv. xsimpl*. destruct HI as (I1&I2&I3). splits.
{ auto. } (* trivial *)
{ auto. } (* trivial *)
{ => j Hj Cj. . } } (* trivial *)
{ => j Hj Cj. forwards~ (r&Hr&Pr): I3 j. exists* r. } } (* trivial *)
{ unfold loop_inv, hinv. intros u. xpull ;=> C' I1 (F1&F2).
rew_set_of_list. xsimpl.
{ splits. (* trivial *)
......
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