Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι be given.
Apply and3I with
30750.. (987b2.. (1216a.. (b5c9f.. x0 x0) (λ x3 . and (bij x0 x0 (λ x4 . f482f.. x3 x4)) (∀ x4 . prim1 x4 x2 ⟶ f482f.. x3 x4 = x4))) (λ x3 x4 . 0fc90.. x0 (λ x5 . f482f.. x4 (f482f.. x3 x5)))),
30750.. (987b2.. (1216a.. (b5c9f.. x0 x0) (λ x3 . and (bij x0 x0 (λ x4 . f482f.. x3 x4)) (∀ x4 . prim1 x4 x1 ⟶ f482f.. x3 x4 = x4))) (λ x3 x4 . 0fc90.. x0 (λ x5 . f482f.. x4 (f482f.. x3 x5)))),
93c99.. (987b2.. (1216a.. (b5c9f.. x0 x0) (λ x3 . and (bij x0 x0 (λ x4 . f482f.. x3 x4)) (∀ x4 . prim1 x4 x2 ⟶ f482f.. x3 x4 = x4))) (λ x3 x4 . 0fc90.. x0 (λ x5 . f482f.. x4 (f482f.. x3 x5)))) (λ x3 . λ x4 : ι → ι → ι . 93c99.. (987b2.. (1216a.. (b5c9f.. x0 x0) (λ x5 . and (bij x0 x0 (λ x6 . f482f.. x5 x6)) (∀ x6 . prim1 x6 x1 ⟶ f482f.. x5 x6 = x6))) (λ x5 x6 . 0fc90.. x0 (λ x7 . f482f.. x6 (f482f.. x5 x7)))) (λ x5 . λ x6 : ι → ι → ι . and (and (987b2.. (1216a.. (b5c9f.. x0 x0) (λ x7 . and (bij x0 x0 (λ x8 . f482f.. x7 x8)) (∀ x8 . prim1 x8 x1 ⟶ f482f.. x7 x8 = x8))) (λ x7 x8 . 0fc90.. x0 (λ x9 . f482f.. x8 (f482f.. x7 x9))) = 987b2.. x5 x4) (4f2b4.. (987b2.. x5 x4))) (Subq x5 x3))) leaving 3 subgoals.
Apply unknownprop_10272f9d8a272cf914054010d8c3a4593cfbbcb7954b0a903e2d867e85e26e68 with
1216a.. (b5c9f.. x0 x0) (λ x3 . and (bij x0 x0 (λ x4 . f482f.. x3 x4)) (∀ x4 . prim1 x4 x2 ⟶ f482f.. x3 x4 = x4)),
λ x3 x4 . 0fc90.. x0 (λ x5 . f482f.. x4 (f482f.. x3 x5)).
Apply unknownprop_303ef75292a7bd9ed5b0c013e4f57cfe7915f538d6e5ad2c3b57bf918b912190 with
x0,
x2.
The subproof is completed by applying L2.
Apply unknownprop_10272f9d8a272cf914054010d8c3a4593cfbbcb7954b0a903e2d867e85e26e68 with
1216a.. (b5c9f.. x0 x0) (λ x3 . and (bij x0 x0 (λ x4 . f482f.. x3 x4)) (∀ x4 . prim1 x4 x1 ⟶ f482f.. x3 x4 = x4)),
λ x3 x4 . 0fc90.. x0 (λ x5 . f482f.. x4 (f482f.. x3 x5)).
Apply unknownprop_303ef75292a7bd9ed5b0c013e4f57cfe7915f538d6e5ad2c3b57bf918b912190 with
x0,
x1.
The subproof is completed by applying H1.
Apply unknownprop_cd20f7dbc591f4f87c87c35509dc2db382cd96f4518c628ca9882a10b2d1671d with
...,
...,
...,
...,
....