Def add ≡ + ∘ [1, 2]

Def mul ≡ × ∘ [1, 2]

Def IP ≡ (/+) ∘ (α ×) ∘ trans

Def append ≡ (null ∘ 1 → 2 ; cons:[hd ∘ 1, append ∘ [tl ∘ 1, 2]])