Let x0 of type ι be given.
Let x1 of type ι → ι be given.
Let x2 of type ι → ι → ο be given.
Let x3 of type ι be given.
Let x4 of type ι be given.
Assume H0:
In (lam 2 (λ x5 . If_i (x5 = 0) x3 x4)) (Sep2 x0 x1 x2).
Let x5 of type ο be given.
Assume H1:
In x3 x0 ⟶ In x4 (x1 x3) ⟶ x2 x3 x4 ⟶ x5.
Apply unknownprop_806479d909a314585644562a92b76db0332e759a7bf7955909b140d76536eec6 with
x0,
x1,
x2,
lam 2 (λ x6 . If_i (x6 = 0) x3 x4),
λ x6 . lam 2 (λ x7 . If_i (x7 = 0) x3 x4) = x6 ⟶ x5 leaving 3 subgoals.
The subproof is completed by applying H0.
Let x6 of type ι be given.
Let x7 of type ι be given.
Assume H3:
In x7 (x1 x6).
Assume H4: x2 x6 x7.
Assume H5:
lam 2 (λ x8 . If_i (x8 = 0) x3 x4) = lam 2 (λ x8 . If_i (x8 = 0) x6 x7).
Apply unknownprop_89c61d8efbfed10cda65f88aa560c75c9a07b94af4fe272148bd98e7547600ec with
x3,
x4,
x6,
x7,
x5 leaving 2 subgoals.
The subproof is completed by applying H5.
Assume H6: x3 = x6.
Assume H7: x4 = x7.
Apply H1 leaving 3 subgoals.
Apply H6 with
λ x8 x9 . In x9 x0.
The subproof is completed by applying H2.
Apply H6 with
λ x8 x9 . In x4 (x1 x9).
Apply H7 with
λ x8 x9 . In x9 (x1 x6).
The subproof is completed by applying H3.
Apply H6 with
λ x8 x9 . x2 x9 x4.
Apply H7 with
λ x8 x9 . x2 x6 x9.
The subproof is completed by applying H4.
Let x6 of type ι → ι → ο be given.
Assume H2:
x6 (lam 2 (λ x7 . If_i (x7 = 0) x3 x4)) (lam 2 (λ x7 . If_i (x7 = 0) x3 x4)).
The subproof is completed by applying H2.