Let x0 of type ι be given.
Let x1 of type ι → ι be given.
Let x2 of type ι be given.
Apply unknownprop_e4362c04e65a765de9cf61045b78be0adc0f9e51a17754420e1088df0891ff67 with
e5b72.. (0fc90.. x0 (λ x3 . prim3 (x1 x3))),
λ x3 . ∀ x4 . prim1 x4 x0 ⟶ prim1 (f482f.. x3 x4) (x1 x4),
x2,
and (∀ x3 . prim1 x3 x2 ⟶ and (cad8f.. x3) (prim1 (f482f.. x3 4a7ef..) x0)) (∀ x3 . prim1 x3 x0 ⟶ prim1 (f482f.. x2 x3) (x1 x3)) leaving 2 subgoals.
The subproof is completed by applying H0.
Apply andI with
∀ x3 . prim1 x3 x2 ⟶ and (cad8f.. x3) (prim1 (f482f.. x3 4a7ef..) x0),
∀ x3 . prim1 x3 x0 ⟶ prim1 (f482f.. x2 x3) (x1 x3) leaving 2 subgoals.
Let x3 of type ι be given.
Apply unknownprop_4134b8a5d866cd7ad711ea569ada0ca0ba949f5cad571bf5782dc7c2d15cdb1c with
0fc90.. x0 (λ x4 . prim3 (x1 x4)),
x2.
The subproof is completed by applying H1.
Apply L4 with
x3.
The subproof is completed by applying H3.
Apply andI with
cad8f.. x3,
prim1 (f482f.. x3 4a7ef..) x0 leaving 2 subgoals.
Apply unknownprop_c8b63681804fba0e817d424dcd4474d1a0cb103b45a1fccf56209850a469b786 with
x0,
λ x4 . prim3 (x1 x4),
x3.
The subproof is completed by applying L5.
Apply L6 with
λ x4 x5 . cad8f.. x4.
The subproof is completed by applying unknownprop_74e7cf1e344053cc0ec428569910c022764085f38ffd3769b306f1021b002573 with
e76d4.. x3,
22ca9.. x3.
Apply unknownprop_a84e7b83bd5a8bec9717474837d8a3466c738bfe80d317693d21dd132b10f7db with
x0,
λ x4 . prim3 (x1 x4),
x3.
The subproof is completed by applying L5.
The subproof is completed by applying H2.