Let x0 of type ι be given.

Let x1 of type ι be given.

Let x2 of type ι → ι → ι be given.

Let x3 of type ι → ι → ι be given.

Assume H0: and (and (30750.. (987b2.. x1 x3)) (30750.. (987b2.. x0 x2))) (93c99.. (987b2.. x1 x3) (λ x4 . λ x5 : ι → ι → ι . 93c99.. (987b2.. x0 x2) (λ x6 . λ x7 : ι → ι → ι . and (and (987b2.. x0 x2 = 987b2.. x6 x5) (4f2b4.. (987b2.. x6 x5))) (Subq x6 x4)))).

Apply H0 with and (987b2.. x0 x2 = 987b2.. x0 x3) (7fe8f.. x1 x3 x0).

Assume H1: and (30750.. (987b2.. x1 x3)) (30750.. (987b2.. x0 x2)).

Apply unknownprop_cd20f7dbc591f4f87c87c35509dc2db382cd96f4518c628ca9882a10b2d1671d with x0, x1, x2, x3, λ x4 x5 : ο . x5 ⟶ and (987b2.. x0 x2 = 987b2.. x0 x3) (7fe8f.. x1 x3 x0).

Assume H2: and (and (987b2.. x0 x2 = 987b2.. x0 x3) (4f2b4.. (987b2.. x0 x3))) (Subq x0 x1).

Apply H2 with and (987b2.. x0 x2 = 987b2.. x0 x3) (7fe8f.. x1 x3 x0).

Assume H3: and (987b2.. x0 x2 = 987b2.. x0 x3) (4f2b4.. (987b2.. x0 x3)).

Apply H3 with Subq x0 x1 ⟶ and (987b2.. x0 x2 = 987b2.. x0 x3) (7fe8f.. x1 x3 x0).

Assume H4: 987b2.. x0 x2 = 987b2.. x0 x3.

Assume H5: 4f2b4.. (987b2.. x0 x3).

Assume H6: Subq x0 x1.

Apply andI with 987b2.. x0 x2 = 987b2.. x0 x3, 7fe8f.. x1 x3 x0 leaving 2 subgoals.

The subproof is completed by applying H4.

Apply andI with 4f2b4.. (987b2.. x0 x3), Subq x0 x1 leaving 2 subgoals.

The subproof is completed by applying H5.

The subproof is completed by applying H6.

■

Proofgold Proof