Let x0 of type ι be given.
Let x1 of type ι be given.
Assume H0:
x1 ∈ {x2 ∈ setexp x0 x0|bij x0 x0 (λ x3 . ap x2 x3)}.
Apply unknownprop_b2dd22a61a18b61173d379dddf1d365ae5cf5bc258fcc9bd0ab516defe84cb3a with
x0,
x1,
explicit_Group_inverse {x2 ∈ setexp x0 x0|bij x0 x0 (λ x3 . ap x2 x3)} (λ x2 x3 . lam x0 (λ x4 . ap x3 (ap x2 x4))) x1 = lam x0 (λ x2 . inv x0 (λ x3 . ap x1 x3) x2) leaving 2 subgoals.
The subproof is completed by applying H0.
Apply H1 with
explicit_Group_inverse {x2 ∈ setexp x0 x0|bij x0 x0 (λ x3 . ap x2 x3)} (λ x2 x3 . lam x0 (λ x4 . ap x3 (ap x2 x4))) x1 = lam x0 (λ x2 . inv x0 (λ x3 . ap x1 x3) x2).
Apply explicit_Group_lcancel with
{x2 ∈ setexp x0 x0|bij x0 x0 (λ x3 . ap x2 x3)},
λ x2 x3 . lam x0 (λ x4 . ap x3 (ap x2 x4)),
x1,
explicit_Group_inverse {x2 ∈ setexp x0 x0|bij x0 x0 (λ x3 . ap x2 x3)} (λ x2 x3 . lam x0 (λ x4 . ap x3 (ap x2 x4))) x1,
lam x0 (λ x2 . inv x0 (λ x3 . ap x1 x3) x2) leaving 5 subgoals.
The subproof is completed by applying explicit_Group_symgroup with x0.
The subproof is completed by applying H0.
Apply explicit_Group_inverse_in with
{x2 ∈ setexp x0 x0|bij x0 x0 (λ x3 . ap x2 x3)},
λ x2 x3 . lam x0 (λ x4 . ap x3 (ap x2 x4)),
x1 leaving 2 subgoals.
The subproof is completed by applying explicit_Group_symgroup with x0.
The subproof is completed by applying H0.
The subproof is completed by applying H3.
set y2 to be ...
set y3 to be ...
Let x4 of type ι → ι → ο be given.
Apply L5 with
λ x5 . x4 x5 y3 ⟶ x4 y3 x5.
Assume H6: x4 y3 y3.
The subproof is completed by applying H6.