Skip to content
Snippets Groups Projects
Commit 49b5dd50 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Use unicide ∧ and ∃.

parent f1f34470
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 1 addition and 1 deletion
tests/algebra.v
+ 1
− 1
View file @ 49b5dd50
...@@ -18,7 +18,7 @@ End tests. ...@@ -18,7 +18,7 @@ End tests.
[2] https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp/merge_requests/38 [2] https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp/merge_requests/38
*) *)
Lemma test_setoid_rewrite : Lemma test_setoid_rewrite :
exists R, @Reflexive Prop R /\ R = iff. ∃ R, @Reflexive Prop R ∧ R = iff.
Proof. Proof.
eexists. split. eexists. split.
- apply _. - apply _.
......
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