We use 0 to witness the existential quantifier.

We use 1 to witness the existential quantifier.

We use n to witness the existential quantifier.

We prove the intermediate claim Hm0: 0 ∈ ω.

An exact proof term for the current goal is (nat_p_omega 0 nat_0).

We prove the intermediate claim Heq00: (0,0) = (0,0).

Use reflexivity.

We prove the intermediate claim Heq1n: (1,n) = (1,n).

Use reflexivity.

We prove the intermediate claim H12: 0 ∈ 2 ∧ 0 ∈ ω.

An exact proof term for the current goal is (andI (0 ∈ 2) (0 ∈ ω) In_0_2 Hm0).

We prove the intermediate claim H123: (0 ∈ 2 ∧ 0 ∈ ω) ∧ 1 ∈ 2.

An exact proof term for the current goal is (andI (0 ∈ 2 ∧ 0 ∈ ω) (1 ∈ 2) H12 In_1_2).

We prove the intermediate claim H1234: ((0 ∈ 2 ∧ 0 ∈ ω) ∧ 1 ∈ 2) ∧ n ∈ ω.

An exact proof term for the current goal is (andI ((0 ∈ 2 ∧ 0 ∈ ω) ∧ 1 ∈ 2) (n ∈ ω) H123 HnOmega).

We prove the intermediate claim H12345: (((0 ∈ 2 ∧ 0 ∈ ω) ∧ 1 ∈ 2) ∧ n ∈ ω) ∧ (0,0) = (0,0).

An exact proof term for the current goal is (andI (((0 ∈ 2 ∧ 0 ∈ ω) ∧ 1 ∈ 2) ∧ n ∈ ω) ((0,0) = (0,0)) H1234 Heq00).

We prove the intermediate claim H123456: ((((0 ∈ 2 ∧ 0 ∈ ω) ∧ 1 ∈ 2) ∧ n ∈ ω) ∧ (0,0) = (0,0)) ∧ (1,n) = (1,n).

An exact proof term for the current goal is (andI ((((0 ∈ 2 ∧ 0 ∈ ω) ∧ 1 ∈ 2) ∧ n ∈ ω) ∧ (0,0) = (0,0)) ((1,n) = (1,n)) H12345 Heq1n).

We prove the intermediate claim Hlex: 0 ∈ 1 ∨ (0 = 1 ∧ 0 ∈ n).

An exact proof term for the current goal is (orIL (0 ∈ 1) (0 = 1 ∧ 0 ∈ n) In_0_1).

Apply andI to the current goal.

An exact proof term for the current goal is H123456.

An exact proof term for the current goal is Hlex.