Simple proofs in Coq taken from More Exercises section of https://www.seas.upenn.edu/~cis500/current/sf/Basics.html

more.v

(* taken from More Exercises sections in https://www.seas.upenn.edu/~cis500/current/sf/Basics.html *)

Theorem identity_fn_applied_twice :
  forall (f : bool -> bool),
    (forall (x : bool), f x = x)
      -> forall (b : bool), f (f b) = b.
Proof.
  intros f H b.
  rewrite -> H.
  rewrite -> H.
  reflexivity.
Qed.

Theorem andb_eq_orb : forall (a b : bool),
  (andb a b = orb a b) -> a = b.
Proof.
   intros a b H.
   destruct a, b.
   - (* case true = true *)
     reflexivity.
   - (* case true = false *)
     inversion H.
   - (* case false = true *)
     inversion H.
   - (* case false = false *)
     reflexivity.
Qed.