unfold Nat.inl at ih ⊢
case step
n : Nat
ih : n.isEven = true → n.half.inl = n
h : (n + 2).isEven = true
⊢ (n + 2).half.inl = n + 2
case step
n : Nat
ih : n.isEven = true → 2 * n.half = n
h : (n + 2).isEven = true
⊢ 2 * (n + 2).half = n + 2