coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: gang chen <gangchen_sh AT yahoo.com>
- To: coq-club AT pauillac.inria.fr
- Subject: [Coq-Club] is "(A<->B)->((F A)<->(F B))" provable ?
- Date: Wed, 13 Feb 2008 15:17:39 -0800 (PST)
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
More precisely, is the assertion
Goal equiv : forall (F : Prop->Prop) (A B : Prop),
(A<->B)->((F A)<->(F B)).
provable ?
--
View this message in context:
http://www.nabble.com/is-%22%28A%3C-%3EB%29-%3E%28%28F-A%29%3C-%3E%28F-B%29%29%22-provable---tp15470251p15470251.html
Sent from the Coq mailing list archive at Nabble.com.
- [Coq-Club] is "(A<->B)->((F A)<->(F B))" provable ?, gang chen
- Re: [Coq-Club] is "(A<->B)->((F A)<->(F B))" provable ?,
Vincent Aravantinos
- Re: [Coq-Club] is "(A<->B)->((F A)<->(F B))" provable ?,
Robin Green
- Re: [Coq-Club] is "(A<->B)->((F A)<->(F B))" provable ?,
Vincent Aravantinos
- Re: [Coq-Club] is "(A<->B)->((F A)<->(F B))" provable ?,
Gyesik Lee
- Re: [Coq-Club] is "(A<->B)->((F A)<->(F B))" provable ?, Andreas Abel
- Re: [Coq-Club] is "(A<->B)->((F A)<->(F B))" provable ?, Bruno Barras
- Re: [Coq-Club] is "(A<->B)->((F A)<->(F B))" provable ?,
Gyesik Lee
- Re: [Coq-Club] is "(A<->B)->((F A)<->(F B))" provable ?,
Vincent Aravantinos
- Re: [Coq-Club] is "(A<->B)->((F A)<->(F B))" provable ?,
Robin Green
- Re: [Coq-Club] is "(A<->B)->((F A)<->(F B))" provable ?,
Vincent Aravantinos
Archive powered by MhonArc 2.6.16.