The Coq mailing list

[mukesh tiwari <mukeshtiwari.iiitm AT gmail.com>]

Hello all,

I am learning Coq and trying to prove  this theorem from Software Foundations by Benjamin Pierce[1].

 Theorem andb_eq_orb : forall (b c : bool),
  ( andb b c = orb b c) ->
  b = c.

Till now I came upto this and not able to solve this further.
Proof.
  intros b c.
  destruct b.
  simpl.
   
I am getting this.

2 subgoals, subgoal 1 (ID 291)
 
  c : bool
  ============================
   c = true -> true = c

subgoal 2 (ID 290) is:
 andb false c = orb false c -> false = c

Could some one please give me some hint to prove this theorem.

Regards,
Mukesh Tiwair

[1] http://www.cis.upenn.edu/~bcpierce/sf/Basics.html