Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι be given.
Apply unknownprop_5c4c172738689d5a3fd02bb243809a41a7c0e7ed334ee0cdfb9155b4865de4da with
x0,
x1,
x2,
∀ x3 . In x3 x0 ⟶ In x3 x1 ⟶ In x3 x2.
Apply unknownprop_738757eec61e36a7ed8ed03b81edd6c58e5dafd21ee5d9ae0df86b9a28226a9f with
x0,
λ x3 . In x3 x1,
λ x3 . In x3 x2,
∀ x3 . In x3 x0 ⟶ In x3 x1 ⟶ In x3 x2.
Assume H0:
∀ x3 . In x3 x0 ⟶ iff (In x3 x1) (In x3 x2).
Let x3 of type ι be given.
Apply unknownprop_d4c6f9663742385071dd283da85a9397dc2dfd0eede50c9fd289b7b23ca97cdd with
In x3 x1,
In x3 x2.
Apply H0 with
x3.
The subproof is completed by applying H1.