Apply unknownprop_f8cb4609f9c174a593de5a10197e2915f5c1a2d9f32ed8d30c3d30b788bb9e1e with λ x0 x1 : ι → ι → ι . ∀ x2 x3 x4 . In x4 x2 ⟶ ∀ x5 . In x5 x3 ⟶ In (lam 2 (λ x6 . If_i (x6 = 0) x4 x5)) (x1 x2 x3).

Let x0 of type ι be given.

Let x1 of type ι be given.

Let x2 of type ι be given.

Assume H0: In x2 x0.

Let x3 of type ι be given.

Assume H1: In x3 x1.

Apply unknownprop_09484b774d66d459105c0920464e409b6d45859c91964dce5b8156bf6c4b7daa with x0, λ x4 . x1, x2, x3 leaving 2 subgoals.

The subproof is completed by applying H0.

The subproof is completed by applying H1.

■

Proofgold Proof