andb_eq_orb.v

(** **** Exercise: 2 stars (andb_eq_orb) *)
(** Prove the following theorem.  (You may want to first prove a
    subsidiary lemma or two.) *)

Lemma orb_always_true :
  forall b,
    orb true b = true.
Proof. reflexivity. Qed.

Lemma andb_always_false : 
  forall b,
    andb false b = false.
Proof. reflexivity. Qed.


Theorem andb_eq_orb : 
  forall (b c : bool),
  (andb b c = orb b c) ->
  b = c.
Proof.
  destruct b.
  intros c.
  intros H.
  rewrite <- orb_always_true with c.
  rewrite <- H.
  destruct c.
  reflexivity.
  reflexivity.
  intros c.
  intros H.
  rewrite <- andb_always_false with c.
  rewrite -> H.
  destruct c.
  reflexivity.
  reflexivity.
Qed.

If you're interested in a shorter solution, I found this one https://github.com/etosch/software_foundations/blob/master/lesson1_Basics.v#L194