diff --git a/tests/algebra.v b/tests/algebra.v index 0ec719eac82be93cfeecc39573369c566b27bfd5..cc94ecc7218f41cf270242e32d8255cc611c9a8e 100644 --- a/tests/algebra.v +++ b/tests/algebra.v @@ -18,7 +18,7 @@ End tests. [2] https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp/merge_requests/38 *) Lemma test_setoid_rewrite : - exists R, @Reflexive Prop R /\ R = iff. + ∃ R, @Reflexive Prop R ∧ R = iff. Proof. eexists. split. - apply _.