basics, 3 stars task

basics.v

Theorem andb_true_id :
  forall a : bool, a = andb true a.
Proof.
  intros []; reflexivity.
Qed.

Theorem orb_false_id :
  forall a : bool, a = orb false a.
Proof.
  intros []; reflexivity.
Qed.

Theorem andb_eq_orb :
  forall (b c : bool),
  (andb b c = orb b c) ->
  b = c.
Proof.
  intros [] c H.
  - rewrite andb_true_id. rewrite H. reflexivity.
  - rewrite orb_false_id. rewrite <- H. reflexivity. 
Qed.