λ-calculus tuple rotl problem

tuple_rotl.txt

Implement a λ-Term named `rotL` that, when applied to a function F, a Church Nat
N, and a Church N-Tuple, returns the same Church N-Tuple, but with elements
shifted left. In other words, create a generic 'rotL<N,F,t>' function for
N-tuples. Example:
- (rotL λf.λx.(f (f x))     λt.(t 1 2))   == λt.(t 2 1)
- (rotL λf.λx.(f (f (f x))) λt.(t 1 2 3)) == λt.(t 2 3 1)
Your final answer must be a λ-Term that implements `rotL` correctly, as follows:
@rotL = term_here

NOTE: Don't omit parenthesis. Each application requires them. Example:
- WRONG: λf. λx. f (f x)
- RIGHT: λf. λx. (f (f x))
- WRONG: (λx. f x) λx.x
- RIGHT: (λx.(f x) λx.x)
- WRONG: λf. λx. λy. (f x y)
- RIGHT: λf. λx. λy. ((f x) y)

ANSWER:

Answer by Gemini 3:

λn. λt. λf. (t ((((n λg. λh. (h (g λa. λb. λc. λd. ((a (b d)) c)))) λu. λx. x) λu. u) f))

Runnable JS:

const rotl = n=>t=>k=>t(x=>n(g=>h=>h(g(q=>r=>s=>q(r(s)))))(u=>f=>f(x))(u=>u)(k));
const show = t => t(a=>b=>c=>d=>[a,b,c,d]);
const len  = s => z => s(s(s(s(z))));
const tup  = t => t(1)(2)(3)(4); // input: λ-tuple (1,2,3,4)
console.log(show(rotl(len)(tup))); // output: λ-tuple (4,1,2,3) 

Interesting. I would have assumed it to find the obvious solution for n-1

n=>t=>k=>t(x=>n(q=>r=>s=>q(r(s)))(u=>u(x))(k))

and adapt it such that it increments the Church n separately or sth
(which is basically what it does, now that I think about it)

Not sure it matters, but fyi such solutions are part of bruijn's standard library (e.g. here), so it might be baked into the model already