induction l
n k l : Nat
⊢ n <<< k <<< l = n <<< (k + l)
case zero
n k : Nat
⊢ n <<< k <<< zero = n <<< (k + zero)

case succ
n k n✝ : Nat
n_ih✝ : n <<< k <<< n✝ = n <<< (k + n✝)
⊢ n <<< k <<< succ n✝ = n <<< (k + succ n✝)