Nat: Type.
Q : (Nat -> Nat) -> Nat -> Nat -> Type.
[a:Nat, f : Nat ->  Nat]  Q f a (f a) --> Nat.