証明記述の例

palette CCC {
  parameter wire X, Y, Z
  node left-eval[X, Y] : (X, X⇒Y) → (Y)
  node decomp-prod[X, Y] : (X×Y) → (X, Y)
  node swap[X, Y] : (X, Y) → (Y, X)

  action LeftCurry[X, Y, Z] ::
    ((X, Y) → (Z)) ~~→ ((Y) → (X⇒Y))

  // ...省略...

  parameter node f: X, Y → Z
  conversion Beta[X, Y, Z, f] ::
    ( (X, LeftCurry[X, Y, Z](f));left-eval[X, Y] ) ~~→ (f)

  // ...省略...

}

• $`(X, X\Rightarrow Y) \to (Y)`$
• $`( X\times Y) \to (X, Y)`$
• $`(\, (X, Y) \to (Z)\,) \rightsquigarrow (\,(Y) \to (X \Rightarrow Y)\,)`$

alias ∧ := ×
declare A, B, C
canvas
  put A∧B, A⇒(B⇒C)
  put CCC.decomp-prod[A, B]
  put CCC.swap[A, B]
  put --after=1 CCC.left-eval[A, B⇒C] 
  put CCC.left-eval[B, C]
  we possess ( A∧B, A⇒(B⇒C) ) → (C)
close
exec CCC.LeftCurry[A∧B, A⇒(B⇒C), C]