Commit 4ddcb65c authored by Joseph Tassarotti's avatar Joseph Tassarotti
Browse files

Remove bad 'simpl' in ticket_clh_refinement.

parent 43c867da
......@@ -54,7 +54,7 @@ Section closed.
{ intros (?&->).
intros a a' n i; by done. }
gid_destruct g as g.
{ simpl in *. intros (?&_). exfalso; eauto. }
{ intros (?&_). exfalso; eauto. }
inversion g.
Grab Existential Variables.
rewrite /Kd. auto.
......
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