Let x0 of type ι be given.

Assume H0: 80242.. x0.

Apply unknownprop_9155775841857cb348ae79731186aa077c95466dd39af675bcbf421e2bc4c9da with x0, 02b90.. (94f9e.. (5246e.. x0) (λ x1 . f4dc0.. x1)) (94f9e.. (23e07.. x0) (λ x1 . f4dc0.. x1)) leaving 2 subgoals.

The subproof is completed by applying H0.

Assume H1: and (and (80242.. (f4dc0.. x0)) (∀ x1 . prim1 x1 (23e07.. x0) ⟶ 099f3.. (f4dc0.. x0) (f4dc0.. x1))) (∀ x1 . prim1 x1 (5246e.. x0) ⟶ 099f3.. (f4dc0.. x1) (f4dc0.. x0)).

Apply H1 with 02b90.. (94f9e.. (5246e.. x0) f4dc0..) (94f9e.. (23e07.. x0) f4dc0..) ⟶ 02b90.. (94f9e.. (5246e.. x0) (λ x1 . f4dc0.. x1)) (94f9e.. (23e07.. x0) (λ x1 . f4dc0.. x1)).

Assume H2: and (80242.. (f4dc0.. x0)) (∀ x1 . prim1 x1 (23e07.. x0) ⟶ 099f3.. (f4dc0.. x0) (f4dc0.. x1)).

Apply H2 with (∀ x1 . prim1 x1 (5246e.. x0) ⟶ 099f3.. (f4dc0.. x1) (f4dc0.. x0)) ⟶ 02b90.. (94f9e.. (5246e.. x0) f4dc0..) (94f9e.. (23e07.. x0) f4dc0..) ⟶ 02b90.. (94f9e.. (5246e.. x0) (λ x1 . f4dc0.. x1)) (94f9e.. (23e07.. x0) (λ x1 . f4dc0.. x1)).

Assume H3: 80242.. (f4dc0.. x0).

Assume H4: ∀ x1 . prim1 x1 (23e07.. x0) ⟶ 099f3.. (f4dc0.. x0) (f4dc0.. x1).

Assume H5: ∀ x1 . prim1 x1 (5246e.. x0) ⟶ 099f3.. (f4dc0.. x1) (f4dc0.. x0).

Assume H6: 02b90.. (94f9e.. (5246e.. x0) f4dc0..) (94f9e.. (23e07.. x0) f4dc0..).

The subproof is completed by applying H6.

■

Proofgold Proof