Let x0 of type ι be given.
Assume H1: x0 = 0 ⟶ ∀ x1 : ο . x1.
Apply unknownprop_4be0565ac5b41f138f7a30d0a9f34a5d126bb341d2eeaa545aa7f0c1552b9722 with
cbf48.. x0,
x0,
λ x1 x2 . x2 = 1 leaving 3 subgoals.
Apply unknownprop_8e324a6fdc5dd93fc7954e55762c3ec235dc1a98306aca944193e8223699b282 with
x0.
The subproof is completed by applying H0.
The subproof is completed by applying H0.
Apply unknownprop_60624b5a99770747095ea0f6821453458503484b58bf76604277214779563c53 with
x0 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.