Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι → ι → ι be given.
Let x3 of type ι → ι → ι be given.
Assume H0:
∀ x4 . In x4 x0 ⟶ ∀ x5 . In x5 x1 ⟶ x2 x4 x5 = x3 x4 x5.
Apply unknownprop_4e431d17235033fd023e568086fb9fd6f3a2be9883f5e2300fe470ca304ea26a with
setprod x0 x1,
λ x4 . x2 (ap x4 0) (ap x4 1),
λ x4 . x3 (ap x4 0) (ap x4 1).
Let x4 of type ι be given.
Apply unknownprop_f8cb4609f9c174a593de5a10197e2915f5c1a2d9f32ed8d30c3d30b788bb9e1e with
λ x5 x6 : ι → ι → ι . In x4 (x6 x0 x1) ⟶ x2 (ap x4 0) (ap x4 1) = x3 (ap x4 0) (ap x4 1).
Assume H1:
In x4 ((λ x5 x6 . lam x5 (λ x7 . x6)) x0 x1).
Apply H0 with
ap x4 0,
ap x4 1 leaving 2 subgoals.
Apply unknownprop_1196af63ee0683855b52ee91758b2774097fb63c424fb057b925104c7b77f7ef with
x0,
λ x5 . x1,
x4.
The subproof is completed by applying H1.
Apply unknownprop_c1205d8a61945e7eb288c6da499403292e9af9500faa25aa1acf052e3d8f0626 with
x0,
λ x5 . x1,
x4.
The subproof is completed by applying H1.