coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: e+coq-club AT x80.org (Emilio Jesús Gallego Arias)
- To: Jonathan Leivent <jonikelee AT gmail.com>
- Cc: coq-club AT inria.fr
- Subject: Re: [Coq-Club] question about universes and equalities
- Date: Tue, 10 May 2016 00:40:59 +0200
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=e+coq-club AT x80.org; spf=Neutral smtp.mailfrom=e+coq-club AT x80.org; spf=None smtp.helo=postmaster AT jiboia.ensmp.fr
- Ironport-phdr: 9a23:uO2OERZmbCk5PUX43KxOx9n/LSx+4OfEezUN459isYplN5qZpcqzbnLW6fgltlLVR4KTs6sC0LqH9fm7EjRRqb+681k8M7V0HycfjssXmwFySOWkMmbcaMDQUiohAc5ZX0Vk9XzoeWJcGcL5ekGA6ibqtW1aJBzzOEJPK/jvHcaK1oLsh7H0osaYO1QArQH+SI0xBS3+lR/WuMgSjNkqAYcK4TyNnEF1ff9Lz3hjP1OZkkW0zM6x+Jl+73YY4Kp5pIYTGZn9KoY/S7VEDD0ge0Q45dPmswWLGQmI4HofX2EbnzJHBgHE6FfxWZKn4QXgse8o1WqROtSzRrQpUxyyv/8tTwXnwGcqMj898WafqMFrHrkTjxuloxFwxMb9eoCcL7stLevmYdoGSD8ZDY5qXCtbD9bkYg==
- Organization: X80 Heavy Industries
Jonathan Leivent
<jonikelee AT gmail.com>
writes:
> Are you sure that thing is inhabited as you say? I can't prove it - I
> end up with subgoals like "True <> False", which I don't think can be
> proven.
Goal True <> False.
Proof. now intros <-. Qed.
should do the job.
Best,
E.
- Re: [Coq-Club] question about universes and equalities, (continued)
- Re: [Coq-Club] question about universes and equalities, Stefan Monnier, 05/09/2016
- Re: [Coq-Club] question about universes and equalities, Jonathan Leivent, 05/09/2016
- Re: [Coq-Club] question about universes and equalities, Jason Gross, 05/09/2016
- Re: [Coq-Club] question about universes and equalities, Jonathan Leivent, 05/10/2016
- Re: [Coq-Club] question about universes and equalities, Clément Pit--Claudel, 05/10/2016
- Re: [Coq-Club] question about universes and equalities, Clément Pit--Claudel, 05/10/2016
- Re: [Coq-Club] question about universes and equalities, Jonathan Leivent, 05/10/2016
- Re: [Coq-Club] question about universes and equalities, Clément Pit--Claudel, 05/10/2016
- Re: [Coq-Club] question about universes and equalities, Jonathan Leivent, 05/10/2016
- Re: [Coq-Club] question about universes and equalities, Jason Gross, 05/10/2016
- Re: [Coq-Club] question about universes and equalities, Jason Gross, 05/09/2016
- Re: [Coq-Club] question about universes and equalities, Jonathan Leivent, 05/09/2016
- Re: [Coq-Club] question about universes and equalities, Stefan Monnier, 05/09/2016
- Re: [Coq-Club] question about universes and equalities, Emilio Jesús Gallego Arias, 05/10/2016
Archive powered by MHonArc 2.6.18.