Let x0 of type ι be given.
Apply and3I with
∀ x1 . x1 ∈ {x2 ∈ setexp x0 x0|bij x0 x0 (λ x3 . ap x2 x3)} ⟶ ∀ x2 . x2 ∈ {x3 ∈ setexp x0 x0|bij x0 x0 (λ x4 . ap x3 x4)} ⟶ (λ x3 x4 . lam x0 (λ x5 . ap x4 (ap x3 x5))) x1 x2 ∈ {x3 ∈ setexp x0 x0|bij x0 x0 (λ x4 . ap x3 x4)},
∀ x1 . x1 ∈ {x2 ∈ setexp x0 x0|bij x0 x0 (λ x3 . ap x2 x3)} ⟶ ∀ x2 . x2 ∈ {x3 ∈ setexp x0 x0|bij x0 x0 (λ x4 . ap x3 x4)} ⟶ ∀ x3 . x3 ∈ {x4 ∈ setexp x0 x0|bij x0 x0 (λ x5 . ap x4 x5)} ⟶ (λ x4 x5 . lam x0 (λ x6 . ap x5 (ap x4 x6))) x1 ((λ x4 x5 . lam x0 (λ x6 . ap x5 (ap x4 x6))) x2 x3) = (λ x4 x5 . lam x0 (λ x6 . ap x5 (ap x4 x6))) ((λ x4 x5 . lam x0 (λ x6 . ap x5 (ap x4 x6))) x1 x2) x3,
∃ x1 . and (x1 ∈ {x2 ∈ setexp x0 x0|bij x0 x0 (λ x3 . ap x2 x3)}) (and (∀ x2 . x2 ∈ {x3 ∈ setexp x0 x0|bij x0 x0 (λ x4 . ap x3 x4)} ⟶ and ((λ x3 x4 . lam x0 (λ x5 . ap x4 (ap x3 x5))) x1 x2 = x2) ((λ x3 x4 . lam x0 (λ x5 . ap x4 (ap x3 x5))) x2 x1 = x2)) (∀ x2 . x2 ∈ {x3 ∈ setexp x0 x0|bij x0 x0 (λ x4 . ap x3 x4)} ⟶ ∃ x3 . and (x3 ∈ {x4 ∈ setexp x0 x0|bij x0 x0 (λ x5 . ap x4 x5)}) (and ((λ x4 x5 . lam x0 (λ x6 . ap x5 (ap x4 x6))) x2 x3 = x1) ((λ x4 x5 . lam x0 (λ x6 . ap x5 (ap x4 x6))) x3 x2 = x1)))) leaving 3 subgoals.
The subproof is completed by applying unknownprop_8c28017e57ab2ec2cae7456a68ed4001fbd633ee80009212ac3e7002fe0a637a with x0.
Let x1 of type ι be given.
Assume H0:
x1 ∈ {x2 ∈ setexp x0 x0|bij x0 x0 (λ x3 . ap x2 x3)}.