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.. x2 (bc82c.. x0 x1) ⟶ or (∃ x3 . and (prim1 x3 (23e07.. x0)) (fe4bb.. x2 (bc82c.. x3 x1))) (∃ x3 . and (prim1 x3 (23e07.. x1)) (fe4bb.. x2 (bc82c.. x0 x3))).
Let x2 of type ι be given.
Apply dneg with
or (∃ x3 . and (prim1 x3 (23e07.. x0)) (fe4bb.. x2 (bc82c.. x3 x1))) (∃ x3 . and (prim1 x3 (23e07.. x1)) (fe4bb.. x2 (bc82c.. x0 x3))).
Apply unknownprop_86d1ac064e08bd36bc8f8c7d3070ea65b389686b3ca603e510b47119b9d626ec with
x2.
Apply unknownprop_13b99fd000490b330591961fc1e419c9f4ce9013dd2d43edb6af3c0a8dc957a3 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 H6.
Apply unknownprop_b2d3cb96a6a882d02e5e57dcfc02559b580d1f8621959f82afe70dc68a4b010f with
x0,
x1,
λ x3 x4 . fe4bb.. ... ... leaving 3 subgoals.
Let x2 of type ι be given.
Apply unknownprop_eac7a6683c5ba7aa6ad74545e4a4f065634321e5b116001d3b7a7c41d91b1bf6 with
bc82c.. x0 x1,
x2,
or (∃ x3 . and (prim1 x3 (23e07.. x0)) (fe4bb.. x2 (bc82c.. x3 x1))) (∃ x3 . and (prim1 x3 (23e07.. x1)) (fe4bb.. x2 (bc82c.. x0 x3))) 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.