Let M and N be given.

Assume HMN.

Let x be given.

Assume Hx.

Let v be given.

Assume Hv.

Apply Hx v Hv to the current goal.

Assume H1: ordinal v.

We will prove ordinal v ∨ ∃i ∈ N, v = {i}.

Apply orIL to the current goal.

An exact proof term for the current goal is H1.

Assume H.

Apply H to the current goal.

Let i be given.

Assume H.

Apply H to the current goal.

Assume Hi: i ∈ M.

Assume H1: v = {i}.

We will prove ordinal v ∨ ∃i ∈ N, v = {i}.

Apply orIR to the current goal.

We use i to witness the existential quantifier.

Apply andI to the current goal.

We will prove i ∈ N.

An exact proof term for the current goal is HMN i Hi.

An exact proof term for the current goal is H1.

∎