Commit c7fe8cd2 authored by Robbert Krebbers's avatar Robbert Krebbers

Some cleanup.

parent 9d0d6825
...@@ -581,15 +581,7 @@ Proof. ...@@ -581,15 +581,7 @@ Proof.
* rewrite NoDup_nil. * rewrite NoDup_nil.
setoid_rewrite elem_of_nil. naive_solver. setoid_rewrite elem_of_nil. naive_solver.
* rewrite !NoDup_cons. * rewrite !NoDup_cons.
setoid_rewrite elem_of_cons. setoid_rewrite elem_of_app. setoid_rewrite elem_of_cons. setoid_rewrite elem_of_app. naive_solver.
split.
destruct IHl.
intros [??].
split.
naive_solver.
naive_solver.
naive_solver.
Qed. Qed.
Global Instance NoDup_proper: Global Instance NoDup_proper:
......
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