An exact proof term for the current goal is (ordsuccI1 1 0 In_0_1).