Let x0 of type ι be given.
Let x1 of type ι → ι be given.
Let x2 of type ι → ι be given.
Assume H0:
∀ x3 . In x3 x0 ⟶ x1 x3 = x2 x3.
Apply unknownprop_c3fe42b21df0810041479a97b374de73f7754e07c8af1c88386a1e7dc0aad10f with
Repl x0 (λ x3 . x1 x3),
Repl x0 (λ x3 . x2 x3).
Let x3 of type ι be given.
Assume H1:
In x3 (Repl x0 (λ x4 . x1 x4)).
Apply unknownprop_89e422bb3b8a01dd209d7f2f210df650a435fc3e6005e0f59c57a5e7a59a6d0e with
x0,
x1,
x3,
In x3 (Repl x0 (λ x4 . x2 x4)) leaving 2 subgoals.
The subproof is completed by applying H1.
Let x4 of type ι be given.
Assume H3: x3 = x1 x4.
Apply H3 with
λ x5 x6 . In x6 (Repl x0 (λ x7 . x2 x7)).
Apply H0 with
x4,
λ x5 x6 . In x6 (Repl x0 (λ x7 . x2 x7)) leaving 2 subgoals.
The subproof is completed by applying H2.
Apply unknownprop_63c308b92260dbfca8c9530846e6836ba3e6be221cc8e80fd61db913e01bdacf with
x0,
x2,
x4.
The subproof is completed by applying H2.