coq-club AT inria.fr

Subject: The Coq mailing list

List archive

From a proof of A and a proof of A -> B, we can infer B. This is the -> elimination rule.

Similarly, from a proof a of A and a proof of forall x : A, P, we can infer P[a/x]. This is the forall elimination rule.

How are these elimination rules manifest in Coq?

Regards,

Jeff.

[Coq-Club] Elimination Rules, Terrell, Jeffrey, 08/06/2014
- Re: [Coq-Club] Elimination Rules, Maxime Dénès, 08/06/2014
  - Re: [Coq-Club] Elimination Rules, Terrell, Jeffrey, 08/07/2014
    - Re: [Coq-Club] Elimination Rules, Arnaud Spiwack, 08/07/2014
      - Re: [Coq-Club] Elimination Rules, Terrell, Jeffrey, 08/08/2014
        
        Re: [Coq-Club] Elimination Rules, Abhishek Anand, 08/08/2014
        
        Re: [Coq-Club] Elimination Rules, Vladimir Voevodsky, 08/09/2014
        
        Message not available
        Re: [Coq-Club] Elimination Rules, Abhishek Anand, 08/10/2014
        Re: [Coq-Club] Elimination Rules, Andrej Bauer, 08/11/2014
        Re: [Coq-Club] Elimination Rules, Andrej Bauer, 08/11/2014
        
        Re: [Coq-Club] Elimination Rules, Abhishek Anand, 08/11/2014