The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

On 08/10/2013 02:24 PM, N. Raghavendra wrote:
> Thanks for that. I now have
> ----------------------------------------------------------------------
> Theorem andb_eq_orb :
>    forall (b c : bool),
>    (andb b c = orb b c) ->
>    b = c.
>
> Proof.
>    intros b c H.
>    destruct b.
>    simpl in H.
>    rewrite ->  H.
>    reflexivity.
>
>    simpl in H.
>    rewrite ->  H.
>    reflexivity.
> Qed.
> ----------------------------------------------------------------------
>    

A shorter proof script is
     destruct b; auto.