Let x0 of type ι be given.
Let x1 of type ι be given.
Apply unknownprop_f04ee3f2db7dade92ee7be101bff40fb89f733bb0c0340f09b616cd72154ad93 with
λ x2 . prim1 (e4431.. x2) (e4431.. (bc82c.. x0 x1)) ⟶ 099f3.. (bc82c.. x0 x1) x2 ⟶ or (∃ x3 . and (prim1 x3 (5246e.. x0)) (fe4bb.. (bc82c.. x3 x1) x2)) (∃ x3 . and (prim1 x3 (5246e.. x1)) (fe4bb.. (bc82c.. x0 x3) x2)).
Let x2 of type ι be given.
Apply dneg with
or (∃ x3 . and (prim1 x3 (5246e.. x0)) (fe4bb.. (bc82c.. x3 x1) x2)) (∃ x3 . and (prim1 x3 (5246e.. x1)) (fe4bb.. (bc82c.. x0 x3) x2)).
Apply unknownprop_86d1ac064e08bd36bc8f8c7d3070ea65b389686b3ca603e510b47119b9d626ec with
x2.
Apply unknownprop_01059785170d3f6ee7ccae83a53df10446a7c0a3edc3b8aae06f45756a2928c3 with
x2,
bc82c.. x0 x1,
x2 leaving 5 subgoals.
The subproof is completed by applying H3.
The subproof is completed by applying L2.
The subproof is completed by applying H3.
The subproof is completed by applying L8.
The subproof is completed by applying H6.
Let x2 of type ι be given.
Apply unknownprop_9139ee2a8df08ed3f37f7756be409060ff2feed4e0a070067f7d01230efaf1e9 with
bc82c.. x0 x1,
x2,
or (∃ x3 . and (prim1 x3 (5246e.. x0)) (fe4bb.. (bc82c.. x3 x1) x2)) (∃ x3 . and (prim1 x3 (5246e.. x1)) (fe4bb.. (bc82c.. x0 x3) x2)) leaving 3 subgoals.
The subproof is completed by applying L2.
The subproof is completed by applying H4.
Apply L3 with
x2 leaving 3 subgoals.
The subproof is completed by applying H5.
The subproof is completed by applying H6.
The subproof is completed by applying H7.