coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Gaetan Gilbert <gaetan.gilbert AT ens-lyon.fr>
- To: coq-club AT inria.fr
- Subject: [Coq-Club] Equality and universes
- Date: Mon, 17 Jul 2017 17:54:19 +0200
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=gaetan.gilbert AT ens-lyon.fr; spf=Neutral smtp.mailfrom=gaetan.gilbert AT ens-lyon.fr; spf=None smtp.helo=postmaster AT labbe.ens-lyon.fr
- Ironport-phdr: 9a23:8DIUeRPz6PXyMN4rYkMl6mtUPXoX/o7sNwtQ0KIMzox0Lfn6rarrMEGX3/hxlliBBdydsKMbzbKO+4nbGkU4qa6bt34DdJEeHzQksu4x2zIaPcieFEfgJ+TrZSFpVO5LVVti4m3peRMNQJW2aFLduGC94iAPERvjKwV1Ov71GonPhMiryuy+4ZPebgFKiTanfb9+MAi9oBnMuMURnYZsMLs6xAHTontPdeRWxGdoKkyWkh3h+Mq+/4Nt/jpJtf45+MFOTav1f6IjTbxFFzsmKHw65NfqtRbYUwSC4GYXX3gMnRpJBwjF6wz6Xov0vyDnuOdxxDWWMMvrRr0yRD+s7bpkSAXwhSkZNzA37WLZhMJ+g61UvB2vqAdyw5LXbYyPKPZyYq3QcNEcSGFcXshRTStBAoakYoUOFeUOI/pYoJP7p1ATrBW+BA2sC/jxxT9Smn/9wKo30+s7Hg7YwAwvBdQOvG7brNX0MKcdSv66zLPUzTjYcfxW3yz95JHMchEhpvGMW6h8ccTLyUQ2EQ7Ok1aeqZT9Mj+I2ekBr3KX4uhiWO61lmIqqgN8riKxyssylIXFnoMYxk7e+Slk3Io5O8e0RFN0bNOnCpdcqiCXOoRwT8g/WW9nojw6xacDuZOjfCgF1pAnxxnHZvyDaYeH+QnsW/iLLThmgnJlY6uzhxKy8EinzO3wTMe00ExSoipElNnDqGwN2gTO5sWIVvdx5EWs1DSV2wzO6+xJI1o4mbTFJ5I/2rIwk4AcsUXHHi/4gkX2i6qWe10r+uey9evnfq/pppmGO497iwH+Nr8hldKlAeQkKQUBQW6b+f+l2L3n/Uz5R7NKguc4kqnDqJzaP9gUpralAw9J1YYu8wqwDzC/0NgBgXYHKE9FdwmcgojyO1DOJej4Au2lj1Stljdr3fHGMaf7DpXDNHiQ2IvmKL168gtXzBc55dFZ/ZNdTL8bc9zpXUqkm9XVEhY/eyO1x+zqEsk1gowXVH6GBOmWMafYvEWUzu8pOKyIdYgT/jjnfat2r8XyhGM0zAdONZKi2oEaPSi1
If one proves [forall A B : Type@{i}, A = B :> Type@{j} -> A = B :> Type@{k}] in the obvious destruct/reflexivity way there is a constraint [j <= k].
Does anyone know of a way to prove it without generating this constraint?
(there are also constraints i <= j and i <= k but those are expected)
--
Gaëtan Gilbert
- [Coq-Club] Equality and universes, Gaetan Gilbert, 07/17/2017
- Re: [Coq-Club] Equality and universes, darktenaibre, 07/19/2017
Archive powered by MHonArc 2.6.18.