Let x0 of type ι → ι → ι be given.
Let x1 of type ι → ι → ι be given.
Apply unknownprop_fd3d2e7f783867b84b25b06a9614a22d40979688c105b0eabc60f25fb84d3565 with
x0,
x1,
λ x2 x3 : ο . x3 = (x0 = x1) leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
Apply prop_ext_2 with
iff (6fb7f.. x0) (6fb7f.. x1),
x0 = x1 leaving 2 subgoals.
Assume H2: x0 = x1.
Apply H2 with
λ x2 x3 : ι → ι → ι . iff (6fb7f.. x3) (6fb7f.. x1).
The subproof is completed by applying iff_refl with
6fb7f.. x1.