# Define a function using another function

I want to define a translation function g from another function f.

Definition trans (f g : Q -> Q) (t : Q) :=
forall q : Q, f (q + t) == g q.


In the above code, I implicitly define a translation g.

However, I'm unsatisfied with this definition.

In the case that a function f is declared, I want to define a translation function explicitly with a fixed distance (for example, 1).

Definition trans (t:nat){A: Type}(f: nat-> A) := fun n => f (t+n).