Proofgold Proof

pf

Let x0 of type ι be given.

Assume H0: x0 ∈ omega.

Let x1 of type ι → ο be given.

Assume H1: x1 0.

Assume H2: ∀ x2 . x2 ∈ omega ⟶ x1 (ordsucc x2).

Apply unknownprop_3e0b8a92ccb367c3a4739497941a42284f473810a33defa291de0bdb90bdba19 with x1, x0 leaving 3 subgoals.

The subproof is completed by applying H1.

Let x2 of type ι be given.

Assume H3: x2 ∈ omega.

Assume H4: x1 x2.

Apply H2 with x2.

The subproof is completed by applying H3.

The subproof is completed by applying H0.

■