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 x2 ⟶ In x3 x1.
Apply unknownprop_738757eec61e36a7ed8ed03b81edd6c58e5dafd21ee5d9ae0df86b9a28226a9f with
x0,
λ x3 . In x3 x1,
λ x3 . In x3 x2,
∀ x3 . In x3 x0 ⟶ In x3 x2 ⟶ In x3 x1.
Assume H0:
∀ x3 . In x3 x0 ⟶ iff (In x3 x1) (In x3 x2).
Let x3 of type ι be given.
Apply unknownprop_d5d9d085d36b1ca4854d01b78e983bcd20b298e2776d1ae6d4a1dc3393a026ac with
In x3 x1,
In x3 x2.
Apply H0 with
x3.
The subproof is completed by applying H1.