Proofgold Proof

pf

Let x0 of type ι be given.

Assume H0: In 0 x0.

Let x1 of type ι be given.

Assume H1: nat_p x1.

Let x2 of type ι be given.

Assume H2: In x2 x1.

Apply unknownprop_573aa2b517130cfa9ec7139c76128b2956a47aa5447b00217b318e88bd21e408 with x0, x2, x1 leaving 2 subgoals.

The subproof is completed by applying H0.

Apply unknownprop_92b4103b83752522eb6c235601eefa2912e3f6395a346e3a7eb52bb5e37ede81 with x1, x2 leaving 2 subgoals.

The subproof is completed by applying H1.

The subproof is completed by applying H2.

■