Axiom extensionality : forall (X Y : Type) (f g : X -> Y),
  (forall x, f x = g x) -> f = g.