Let x0 of type ι be given.
Apply unknownprop_d0b18a67181e900ea67f7a0ba30a861268ef122d83dee9e0402983f02611aa3f with
x0,
28f8d.. x0 ∈ real leaving 2 subgoals.
The subproof is completed by applying H0.
Let x1 of type ι be given.
Let x2 of type ι be given.
Apply H3 with
λ x3 x4 . 28f8d.. x4 ∈ real.
Apply unknownprop_b9b7bfb6c9b892d1b6018106403bf15df7213abab01ccecd88c7179d2ef8e566 with
x1,
x2,
λ x3 x4 . x4 ∈ real leaving 3 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
The subproof is completed by applying H1.