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