ssreflect - Re: [ssreflect] forall over fintype

Subject: Ssreflect Users Discussion List

List archive

Re: [ssreflect] forall over fintype

From: "John Wiegley" <>
To:
Subject: Re: [ssreflect] forall over fintype
Date: Sun, 30 Nov 2014 15:42:11 -0600
Organization: New Artisans LLC

>>>>> Emilio Jesús Gallego Arias <> writes:

> Goal [forall i : 'I_5, i < 5].
> Proof.
> rewrite /FiniteQuant.all /FiniteQuant.quant0b /pred0b cardE.
> by rewrite /(enum _) unlock /= /ord_enum /= !insubT.
> Qed.

That proof seems rather long, given that i : 'I_5 implies i < 5.

John

[ssreflect] forall over fintype, Arthur Azevedo de Amorim, 11/30/2014
- Re: [ssreflect] forall over fintype, Frederic Chyzak, 11/30/2014
  - Re: [ssreflect] forall over fintype, Enrico Tassi, 11/30/2014
    - Re: [ssreflect] forall over fintype, Arthur Azevedo de Amorim, 11/30/2014
      - Re: [ssreflect] forall over fintype, Frederic Chyzak, 11/30/2014
      - Re: [ssreflect] forall over fintype, Emilio Jesús Gallego Arias, 11/30/2014
        
        Re: [ssreflect] forall over fintype, John Wiegley, 11/30/2014
        
        Re: [ssreflect] forall over fintype, Arthur Azevedo de Amorim, 11/30/2014

List archive

Re: [ssreflect] forall over fintype