diff --git a/tests/typeclasses.v b/tests/typeclasses.v index 6e31f52974a54dcbc9025cbc40b4e69ac3e25bf6..899518d58e83d8427e42fb3ce1a0196fbaa24c74 100644 --- a/tests/typeclasses.v +++ b/tests/typeclasses.v @@ -9,7 +9,7 @@ From stdpp Require Import prelude. [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 _.