Let x0 of type ι → ι → CT2 ι 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.
Let x5 of type ι → ι be given.
Let x6 of type ι → ι be given.
Apply H0 with
x1,
x4,
λ x7 x8 . If_i (x7 = x1) (x5 x8) (x2 x7 x8),
λ x7 x8 . If_i (x7 = x1) (x6 x8) (x3 x7 x8) leaving 4 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H3.
Let x7 of type ι be given.
Let x8 of type ι be given.
Claim L7: x7 = x1 ⟶ ∀ x9 : ο . x9
Apply unknownprop_72d31fc7898fbfa047b15bdf294e41aa3a85b60f216ad9214f5c72146be87fda with
x1,
x7 leaving 2 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H5.
Apply If_i_0 with
x7 = x1,
x5 x8,
x2 x7 x8,
λ x9 x10 . x10 = If_i (x7 = x1) (x6 x8) (x3 x7 x8) leaving 2 subgoals.
The subproof is completed by applying L7.
Apply If_i_0 with
x7 = x1,
x6 x8,
x3 x7 x8,
λ x9 x10 . x2 x7 x8 = x10 leaving 2 subgoals.
The subproof is completed by applying L7.
Apply H2 with
x7,
λ x9 x10 : ι → ι . x10 x8 = x3 x7 x8 leaving 2 subgoals.
The subproof is completed by applying H5.
Let x9 of type ι → ι → ο be given.
Assume H8: x9 (x3 x7 x8) (x3 x7 x8).
The subproof is completed by applying H8.
Let x7 of type ι be given.
Apply If_i_1 with
x1 = x1,
x5 x7,
x2 x1 x7,
λ x8 x9 . x9 = If_i (x1 = x1) (x6 x7) (x3 x1 x7) leaving 2 subgoals.
Let x8 of type ι → ι → ο be given.
Assume H6: x8 x1 x1.
The subproof is completed by applying H6.
Apply If_i_1 with
x1 = x1,
x6 x7,
x3 x1 x7,
λ x8 x9 . x5 x7 = x9 leaving 2 subgoals.
Let x8 of type ι → ι → ο be given.
Assume H6: x8 x1 x1.
The subproof is completed by applying H6.
Apply H4 with
x7.
The subproof is completed by applying H5.