Let x0 of type ο be given.
Let x1 of type ο be given.
Apply unknownprop_535a42de1055bca61f176bc11115db76b3356ad18505799408acb5bdbd2addc1 with
λ x2 x3 : ο → ο → ο . x3 x0 x1 ⟶ iff x1 x0.
Assume H0:
(λ x2 x3 : ο . and (x2 ⟶ x3) (x3 ⟶ x2)) x0 x1.
Apply andE with
x0 ⟶ x1,
x1 ⟶ x0,
iff x1 x0 leaving 2 subgoals.
The subproof is completed by applying H0.
Assume H1: x0 ⟶ x1.
Assume H2: x1 ⟶ x0.
Apply unknownprop_a818f53272de918398012791887b763f90bf043f961a4f625d98076ca0b8b392 with
x1,
x0 leaving 2 subgoals.
The subproof is completed by applying H2.
The subproof is completed by applying H1.