Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι → ο be given.
Let x3 of type ι → ο be given.
Apply unknownprop_0061f7d7cc7224d66e31f046473573b0f6090fa03a4a5550b0992c7403d46f83 with
x0,
x2,
λ x4 x5 . 40dde.. x5 (λ x6 . prim1 x6 (09072.. x0 x2)) (e4431.. (09072.. x1 x3)) (λ x6 . prim1 x6 (09072.. x1 x3)) ⟶ 40dde.. x0 x2 x1 x3 leaving 2 subgoals.
The subproof is completed by applying H0.
Apply unknownprop_0061f7d7cc7224d66e31f046473573b0f6090fa03a4a5550b0992c7403d46f83 with
x1,
x3,
λ x4 x5 . 40dde.. x0 (λ x6 . prim1 x6 (09072.. x0 x2)) x5 (λ x6 . prim1 x6 (09072.. x1 x3)) ⟶ 40dde.. x0 x2 x1 x3 leaving 2 subgoals.
The subproof is completed by applying H1.
Apply unknownprop_516ec77a0547bdde87f302357c77a8c500e4737d03bed523bd783f1c87c1572b with
x0,
x1,
x2,
λ x4 . prim1 x4 (09072.. x0 x2),
x3 leaving 4 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
Apply PNoEq_sym_ with
x0,
λ x4 . prim1 x4 (09072.. x0 x2),
x2.
Apply unknownprop_8ab8782df8e80eb287fd4c918f7b35b584f8954d0de002e6915e8d87848fc5f4 with
x0,
x2.
The subproof is completed by applying H0.
Apply unknownprop_8400f668ce579075dd52a6b0bc8eaa2c816f68129d64497b65439b55d60266f7 with
x0,
x1,
λ x4 . prim1 x4 (09072.. x0 x2),
λ x4 . prim1 x4 (09072.. x1 x3),
x3 leaving 4 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
Apply unknownprop_8ab8782df8e80eb287fd4c918f7b35b584f8954d0de002e6915e8d87848fc5f4 with
x1,
x3.
The subproof is completed by applying H1.