Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι be given.
Apply unknownprop_303ef75292a7bd9ed5b0c013e4f57cfe7915f538d6e5ad2c3b57bf918b912190 with
x0,
x1.
The subproof is completed by applying H0.
Apply unknownprop_18724cb817cb481b8967b1efe13d39d42daa75ec771890da7ad3a6b6981daf0e with
1216a.. (b5c9f.. x0 x0) (λ x2 . bij x0 x0 (λ x3 . f482f.. x2 x3)),
λ x2 x3 . 0fc90.. x0 (λ x4 . f482f.. x3 (f482f.. x2 x4)).
The subproof is completed by applying unknownprop_bc372826b7f0da52f3a8a3ea86862b41fc91267615627787d3fb4a389b8c72dc with x0.
Apply unknownprop_8b9f561399e269db803fe2eecd073d07a2901172a21a3c5747e20aa002026685 with
1216a.. (b5c9f.. x0 x0) (λ x2 . bij x0 x0 (λ x3 . f482f.. x2 x3)),
λ x2 x3 . 0fc90.. x0 (λ x4 . f482f.. x3 (f482f.. x2 x4)),
1216a.. (b5c9f.. x0 x0) (λ x2 . and (bij x0 x0 (λ x3 . f482f.. x2 x3)) (∀ x3 . prim1 x3 x1 ⟶ f482f.. x2 x3 = x3)) leaving 5 subgoals.
The subproof is completed by applying L7.
The subproof is completed by applying L1.
The subproof is completed by applying L3.
The subproof is completed by applying L5.
The subproof is completed by applying L6.