Let x0 of type ι be given.

Let x1 of type ι be given.

Assume H0: Subq x1 x0.

Apply unknownprop_4190872fa06d0bf5579d980e584f8037d61dd3b86edc80c9dfe631305f077d16 with x0, x1, 4f2b4.. (987b2.. (1216a.. (b5c9f.. x0 x0) (λ x2 . and (bij x0 x0 (λ x3 . f482f.. x2 x3)) (∀ x3 . prim1 x3 x1 ⟶ f482f.. x2 x3 = x3))) (λ x2 x3 . 0fc90.. x0 (λ x4 . f482f.. x3 (f482f.. x2 x4)))) leaving 2 subgoals.

The subproof is completed by applying H0.

Assume H1: 4f2b4.. (987b2.. (1216a.. (b5c9f.. x0 x0) (λ x2 . and (bij x0 x0 (f482f.. x2)) (∀ x3 . prim1 x3 x1 ⟶ f482f.. x2 x3 = x3))) (λ x2 x3 . 0fc90.. x0 (λ x4 . f482f.. x3 (f482f.. x2 x4)))).

Assume H2: Subq (1216a.. (b5c9f.. x0 x0) (λ x2 . and (bij x0 x0 (f482f.. x2)) (∀ x3 . prim1 x3 x1 ⟶ f482f.. x2 x3 = x3))) (1216a.. (b5c9f.. x0 x0) (λ x2 . bij x0 x0 (f482f.. x2))).

The subproof is completed by applying H1.

■

Proofgold Proof