Let x0 of type ι be given.
Let x1 of type ι → ι be given.
Let x2 of type ι → ι → ο be given.
Let x3 of type ι → ι → ο be given.
Assume H0:
∀ x4 . In x4 x0 ⟶ ∀ x5 . In x5 (x1 x4) ⟶ iff (x2 x4 x5) (x3 x4 x5).
Apply unknownprop_dc859aa944b71f2e96afeef1fac64e697ab40ad05d9c94301304ef705cd0a5c3 with
Sep2 x0 x1 x2,
Sep2 x0 x1 x3 leaving 3 subgoals.
The subproof is completed by applying unknownprop_bd77e326313d7b8aa8e999f775ae7b4efcbb3023ecf450ebd8fb10b2e4097b63 with x0, x1, x2.
The subproof is completed by applying unknownprop_bd77e326313d7b8aa8e999f775ae7b4efcbb3023ecf450ebd8fb10b2e4097b63 with x0, x1, x3.
Let x4 of type ι be given.
Let x5 of type ι be given.
Apply unknownprop_a818f53272de918398012791887b763f90bf043f961a4f625d98076ca0b8b392 with
In (lam 2 (λ x6 . If_i (x6 = 0) x4 x5)) (Sep2 x0 x1 x2),
In (lam 2 (λ x6 . If_i (x6 = 0) x4 x5)) (Sep2 x0 x1 x3) leaving 2 subgoals.
Assume H1:
In (lam 2 (λ x6 . If_i (x6 = 0) x4 x5)) (Sep2 x0 x1 x2).
Apply unknownprop_c017a644eb6411fee34aba2858ad95d7edc6f065e01505f0c19557e300a42f32 with
x0,
x1,
x2,
x4,
x5,
In (lam 2 (λ x6 . If_i (x6 = 0) x4 x5)) (Sep2 x0 x1 x3) leaving 2 subgoals.
The subproof is completed by applying H1.
Assume H3:
In x5 (x1 x4).
Assume H4: x2 x4 x5.
Apply unknownprop_ea1656dcf618ea522a0b186aaeaab5d7e061cc4df06fdc86629bfb7dbd0ffe6f with
x0,
x1,
x3,
x4,
x5 leaving 3 subgoals.
The subproof is completed by applying H2.
The subproof is completed by applying H3.
Apply unknownprop_6e9d790c24657bc527a0f62de036403ca00386b366ddc02915f8c3a4de529eee with
x2 x4 x5,
x3 x4 x5,
x3 x4 x5 leaving 3 subgoals.
Apply H0 with
x4,
x5 leaving 2 subgoals.
The subproof is completed by applying H2.
The subproof is completed by applying H3.
Assume H5: x2 x4 x5.
Assume H6: x3 x4 x5.
The subproof is completed by applying H6.
Assume H5:
not (x2 x4 x5).
Assume H6:
not (x3 x4 x5).
Apply FalseE with
x3 x4 x5.
Apply notE with
x2 x4 x5 leaving 2 subgoals.
The subproof is completed by applying H5.
The subproof is completed by applying H4.
Assume H1:
In (lam 2 (λ x6 . If_i (x6 = 0) x4 x5)) (Sep2 x0 x1 x3).
Apply unknownprop_c017a644eb6411fee34aba2858ad95d7edc6f065e01505f0c19557e300a42f32 with
x0,
x1,
x3,
x4,
x5,
In (lam 2 (λ x6 . If_i (x6 = 0) x4 x5)) (Sep2 x0 x1 x2) leaving 2 subgoals.
The subproof is completed by applying H1.
Assume H3:
In x5 (x1 x4).
Assume H4: x3 x4 x5.
Apply unknownprop_ea1656dcf618ea522a0b186aaeaab5d7e061cc4df06fdc86629bfb7dbd0ffe6f with
x0,
x1,
x2,
x4,
x5 leaving 3 subgoals.
The subproof is completed by applying H2.
The subproof is completed by applying H3.
Apply unknownprop_6e9d790c24657bc527a0f62de036403ca00386b366ddc02915f8c3a4de529eee with
x2 x4 x5,
x3 x4 x5,
x2 x4 x5 leaving 3 subgoals.
Apply H0 with
x4,
x5 leaving 2 subgoals.
The subproof is completed by applying H2.
The subproof is completed by applying H3.
Assume H5: x2 x4 x5.
Assume H6: x3 x4 x5.
The subproof is completed by applying H5.
Assume H5:
not (x2 x4 x5).
Assume H6:
not (x3 x4 x5).
Apply FalseE with
x2 x4 x5.
Apply notE with
x3 x4 x5 leaving 2 subgoals.
The subproof is completed by applying H6.
The subproof is completed by applying H4.