rewrite the current goal using beta 2 (λi ⇒ if i = 0 then x0 else x1) 0 In_0_2 (from left to right).