The Coq mailing list

[Jean-Francois Monin <jean-francois.monin AT imag.fr>]

Because A <-> B, by definition, is A -> B /\ B-> A.
f : A -> B can be applied to an argument x:A,
g: A <-> B cannot, only (fst g) can.

Hope this helps,
JF

On Mon, Jul 25, 2011 at 10:27:21AM +0800, Ly Kim Quyen (Gwenhael) wrote:
> Lemma bcoef_pos_ok : forall n (p : poly n), bcoef_pos n p = true <->
> coef_pos n p.
> 
> Lemma bcoef_pos_ok_2 : forall n (p : poly n), bcoef_pos n p = true ->
> coef_pos n p.
> [...]
> 
> My question is: Why I cannot apply the lemma *bcoef_pos_ok* in this
> definition?
> I got the error saying that: "*The expression "bcoef_pos_ok n p" of type
> "bcoef_pos n p = true <-> coef_pos n p"
> cannot be applied to the term  "h0" : "bcoef_pos n p = true"* "
> But if I am using the lemma *bcoef_pos_ok_2* it works.
> 
> Thank you very much,
> Gwen