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✝)