%(A:*) @(n:Nat) @(f:@(x:A) A) @(x:A) A