Hola.
No, un término de este tipo (omitendo los tipos en el término) sería:
λf.λt1.λt2. ((f t2) t1)
En Coq:
Variable A B C: Set.
Definition term := fun (f: A -> B -> C) (t1: B) (t2: A) => f t2 t1.
Check term. (* (A -> B -> C) -> B -> A -> C *)
Saludos, Carlos