Apply unknownprop_1695e2f877b363b9b1913ee7a1d28c6ecf021bbb0a05d49f31d2841490fcb6d0 with λ x0 x1 x2 . ∀ x3 : ο . (x0 = c4def.. ⟶ x1 = x2 ⟶ x3) ⟶ (∀ x4 x5 x6 x7 x8 . d7d78.. x4 x6 x7 ⟶ d7d78.. x5 x7 x8 ⟶ x0 = 6b90c.. x4 x5 ⟶ x1 = x6 ⟶ x2 = x8 ⟶ x3) ⟶ (x0 = c9248.. ⟶ x2 = 236c6.. ⟶ x3) ⟶ (∀ x4 x5 x6 . d7d78.. x4 x5 x6 ⟶ x0 = a6e19.. x4 ⟶ x1 = x5 ⟶ x2 = 0b8ef.. x6 ⟶ x3) ⟶ (∀ x4 x5 x6 . d7d78.. x4 x5 x6 ⟶ x0 = 2fe34.. x4 ⟶ x1 = x5 ⟶ x2 = 6c5f4.. x6 ⟶ x3) ⟶ (∀ x4 x5 x6 x7 x8 . e05e6.. x5 ⟶ d7d78.. x4 (cfc98.. x6 x7) x8 ⟶ x0 = 3e00e.. x4 x5 ⟶ x1 = cfc98.. (0b8ef.. x6) x7 ⟶ x2 = x8 ⟶ x3) ⟶ (∀ x4 x5 x6 x7 x8 . e05e6.. x4 ⟶ d7d78.. x5 (cfc98.. x6 x7) x8 ⟶ x0 = 3e00e.. x4 x5 ⟶ x1 = cfc98.. (6c5f4.. x6) x7 ⟶ x2 = x8 ⟶ x3) ⟶ (∀ x4 x5 x6 x7 x8 . d7d78.. x4 x6 x7 ⟶ d7d78.. x5 x6 x8 ⟶ x0 = f9341.. x4 x5 ⟶ x1 = x6 ⟶ x2 = cfc98.. x7 x8 ⟶ x3) ⟶ (∀ x4 x5 x6 x7 . d7d78.. x4 x5 x7 ⟶ x0 = 1fa6d.. x4 ⟶ x1 = cfc98.. x5 x6 ⟶ x2 = x7 ⟶ x3) ⟶ (∀ x4 x5 x6 x7 . d7d78.. x4 x6 x7 ⟶ x0 = 3a365.. x4 ⟶ x1 = cfc98.. x5 x6 ⟶ x2 = x7 ⟶ x3) ⟶ x3 leaving 10 subgoals.

Let x0 of type ι be given.

Assume H0: d7d78.. c4def.. x0 x0.

Let x1 of type ο be given.

Assume H1: c4def.. = c4def.. ⟶ x0 = x0 ⟶ x1.

Assume H2: ∀ x2 x3 x4 x5 x6 . d7d78.. x2 x4 x5 ⟶ d7d78.. x3 x5 x6 ⟶ c4def.. = 6b90c.. x2 x3 ⟶ x0 = x4 ⟶ x0 = x6 ⟶ x1.

Assume H3: c4def.. = c9248.. ⟶ x0 = 236c6.. ⟶ x1.

Assume H4: ∀ x2 x3 x4 . d7d78.. x2 x3 x4 ⟶ c4def.. = a6e19.. x2 ⟶ x0 = x3 ⟶ x0 = 0b8ef.. x4 ⟶ x1.

Assume H5: ∀ x2 x3 x4 . d7d78.. x2 x3 x4 ⟶ c4def.. = 2fe34.. x2 ⟶ x0 = x3 ⟶ x0 = 6c5f4.. x4 ⟶ x1.

Assume H6: ∀ x2 x3 x4 x5 x6 . ... ⟶ ... ⟶ c4def.. = 3e00e.. x2 x3 ⟶ x0 = cfc98.. (0b8ef.. x4) x5 ⟶ x0 = x6 ⟶ x1.

...

■

Proofgold Proof