\forall x,y,f. x=y \to (f x) = (f y)