(** * Prelude: an introduction to using Coq *)

Definition id (a : Type) : a -> a :=
  fun x => x.

Definition const (a : Type) (b : Type) : a -> b -> a :=
  fun x y => x.

Print const.

Check (id _ const).

About id.

Lemma silly : (fun x y => x) 3 5 = 3.
  Proof.
    simpl.
    reflexivity.
  Qed.

Extraction Language Haskell.
Extraction id. 
Extraction const.