Let x0 of type ι be given.
Let x1 of type ι be given.
Assume H2: x1 = 0 ⟶ ∀ x2 : ο . x2.
Apply unknownprop_4be0565ac5b41f138f7a30d0a9f34a5d126bb341d2eeaa545aa7f0c1552b9722 with
x1,
bf082.. x0 x1,
λ x2 x3 . x3 = x0 leaving 3 subgoals.
The subproof is completed by applying H1.
Apply unknownprop_7e109fe8a86bc772f947345bca731e46765cdd64b4b42e3642bf3487c4a64010 with
x0,
x1 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
Apply unknownprop_61f618358c6caba0be539f7d9823aaa498c1bb68a19c0266545b6a0ee0013f72 with
x0,
x1 leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying H2.