Let m be given.
Assume Hm.
Let n be given.
Assume Hn.
Let m' be given.
Assume Hm'.
Let n' be given.
Assume Hn'.
Assume H1: nat_pair m n = nat_pair m' n'.
We prove the intermediate claim L1: m = m'.
An exact proof term for the current goal is nat_pair_0 m Hm n Hn m' Hm' n' Hn' H1.
We prove the intermediate claim L2nS: SNo (2 * n).
An exact proof term for the current goal is SNo_mul_SNo 2 n SNo_2 (omega_SNo n Hn).
We prove the intermediate claim L2n1S: SNo (2 * n + 1).
An exact proof term for the current goal is SNo_add_SNo (2 * n) 1 ?? SNo_1.
We prove the intermediate claim L2n'S: SNo (2 * n').
An exact proof term for the current goal is SNo_mul_SNo 2 n' SNo_2 (omega_SNo n' Hn').
We prove the intermediate claim L2n'1S: SNo (2 * n' + 1).
An exact proof term for the current goal is SNo_add_SNo (2 * n') 1 ?? SNo_1.
We will prove n = n'.
Apply mul_SNo_nonzero_cancel_L 2 n n' SNo_2 neq_2_0 (omega_SNo n Hn) (omega_SNo n' Hn') to the current goal.
We will prove 2 * n = 2 * n'.
Apply add_SNo_cancel_R (2 * n) 1 (2 * n') ?? SNo_1 ?? to the current goal.
We will prove 2 * n + 1 = 2 * n' + 1.
We prove the intermediate claim L2mS: SNo (2 ^ m).
An exact proof term for the current goal is SNo_exp_SNo_nat 2 SNo_2 m (omega_nat_p m Hm).
We prove the intermediate claim L2mn0: 2 ^ m ≠ 0.
Assume H2: 2 ^ m = 0.
Apply neq_1_0 to the current goal.
We will prove 1 = 0.
rewrite the current goal using mul_SNo_eps_power_2 m (omega_nat_p m Hm) (from right to left).
We will prove eps_ m * 2 ^ m = 0.
rewrite the current goal using H2 (from left to right).
We will prove eps_ m * 0 = 0.
An exact proof term for the current goal is mul_SNo_zeroR (eps_ m) (SNo_eps_ m Hm).
Apply mul_SNo_nonzero_cancel_L (2 ^ m) (2 * n + 1) (2 * n' + 1) ?? ?? ?? ?? to the current goal.
We will prove (2 ^ m) * (2 * n + 1) = (2 ^ m) * (2 * n' + 1).
rewrite the current goal using L1 (from left to right) at position 2.
An exact proof term for the current goal is H1.
∎