Let x0 of type ι be given.
Apply explicit_Group_identity_unique with
1216a.. (b5c9f.. x0 x0) (λ x1 . bij x0 x0 (λ x2 . f482f.. x1 x2)),
λ x1 x2 . 0fc90.. x0 (λ x3 . f482f.. x2 (f482f.. x1 x3)),
explicit_Group_identity (1216a.. (b5c9f.. x0 x0) (λ x1 . bij x0 x0 (λ x2 . f482f.. x1 x2))) (λ x1 x2 . 0fc90.. x0 (λ x3 . f482f.. x2 (f482f.. x1 x3))),
0fc90.. x0 (λ x1 . x1) leaving 4 subgoals.
Apply explicit_Group_identity_in with
1216a.. (b5c9f.. x0 x0) (λ x1 . bij x0 x0 (λ x2 . f482f.. x1 x2)),
λ x1 x2 . 0fc90.. x0 (λ x3 . f482f.. x2 (f482f.. x1 x3)).
The subproof is completed by applying unknownprop_bc372826b7f0da52f3a8a3ea86862b41fc91267615627787d3fb4a389b8c72dc with x0.
The subproof is completed by applying unknownprop_aae29273795af056cc88f6696316efac16ebbd2fa5d1e2bf82aeb4ac67a3948e with x0.
Apply explicit_Group_identity_lid with
1216a.. (b5c9f.. x0 x0) (λ x1 . bij x0 x0 (λ x2 . f482f.. x1 x2)),
λ x1 x2 . 0fc90.. x0 (λ x3 . f482f.. x2 (f482f.. x1 x3)).
The subproof is completed by applying unknownprop_bc372826b7f0da52f3a8a3ea86862b41fc91267615627787d3fb4a389b8c72dc with x0.
Let x1 of type ι be given.
Apply unknownprop_e4362c04e65a765de9cf61045b78be0adc0f9e51a17754420e1088df0891ff67 with
b5c9f.. x0 x0,
λ x2 . bij x0 x0 (λ x3 . f482f.. x2 x3),
x1,
0fc90.. x0 (λ x2 . f482f.. (0fc90.. x0 (λ x3 . x3)) (f482f.. x1 x2)) = x1 leaving 2 subgoals.
The subproof is completed by applying H0.
Let x2 of type ι be given.
Apply unknownprop_c16431872c3632171d44e2f1264db15ffa03222bbf17533f9dd2e335f0e49cd9 with
x0,
λ x3 . x0,
x1,
x2 leaving 2 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H3.
Apply unknownprop_37fcf738b3aad2297378a2358f205c1613763d36e48c6969ecd725fbc7fdfb27 with
x0,
λ x2 . x0,
0fc90.. x0 (λ x2 . f482f.. (0fc90.. x0 (λ x3 . x3)) (f482f.. x1 x2)),
x1 leaving 3 subgoals.
Apply unknownprop_78f4273a7b4d13f02d77d194b65be481121674fd021f4ffb88d69be4bcd0ab71 with
x0,
λ x2 . x0,
λ x2 . f482f.. (0fc90.. x0 (λ x3 . x3)) (f482f.. x1 x2).
Let x2 of type ι be given.
Apply unknownprop_b456609235d152f08bccfce314d541d7c44f3716137c00b0ce21cf467ba83d17 with
x0,
λ x3 . x3,
f482f.. x1 x2,
λ x3 x4 . prim1 x4 x0 leaving 2 subgoals.
Apply L3 with
x2.
The subproof is completed by applying H4.
Apply L3 with
x2.
The subproof is completed by applying H4.
The subproof is completed by applying H1.
Let x2 of type ι be given.
Apply unknownprop_b456609235d152f08bccfce314d541d7c44f3716137c00b0ce21cf467ba83d17 with
x0,
λ x3 . f482f.. (0fc90.. x0 (λ x4 . x4)) (f482f.. x1 x3),
x2,
λ x3 x4 . x4 = f482f.. x1 x2 leaving 2 subgoals.
The subproof is completed by applying H4.
Apply unknownprop_b456609235d152f08bccfce314d541d7c44f3716137c00b0ce21cf467ba83d17 with
x0,
λ x3 . x3,
f482f.. x1 x2.
Apply L3 with
x2.
The subproof is completed by applying H4.