Alphabet

lk:(W → E) → E
ud:W → E → E

Variables

X:E
Y:W
U:W
V:E
W:W
J:W → E
F1:W → W → E

Rules

lk · (λ%X:W.ud · %X · X)⇒X
ud · Y · (ud · U · V)⇒ud · U · V
ud · W · (lk · (λ%Y:W.J · %Y))⇒ud · W · (J · W)
lk · (λ%Z:W.lk · (λ%U:W.F1 · %U · %Z))⇒lk · (λ%V:W.F1 · %V · %V)