Apply unknownprop_85336ee07ace71a942dc508d3b8c851d9d6bb88511443b7dafbf11b71c263f4d with λ x0 . or (x0 = 4a7ef..) (∃ x1 . and (ba9d8.. x1) (x0 = 4ae4a.. x1)) leaving 2 subgoals.

Apply orIL with 4a7ef.. = 4a7ef.., ∃ x0 . and (ba9d8.. x0) (4a7ef.. = 4ae4a.. x0).

Let x0 of type ι → ι → ο be given.

Assume H0: x0 4a7ef.. 4a7ef...

The subproof is completed by applying H0.

Let x0 of type ι be given.

Assume H0: ba9d8.. x0.

Assume H1: or (x0 = 4a7ef..) (∃ x1 . and (ba9d8.. x1) (x0 = 4ae4a.. x1)).

Apply orIR with 4ae4a.. x0 = 4a7ef.., ∃ x1 . and (ba9d8.. x1) (4ae4a.. x0 = 4ae4a.. x1).

Let x1 of type ο be given.

Assume H2: ∀ x2 . and (ba9d8.. x2) (4ae4a.. x0 = 4ae4a.. x2) ⟶ x1.

Apply H2 with x0.

Apply andI with ba9d8.. x0, 4ae4a.. x0 = 4ae4a.. x0 leaving 2 subgoals.

The subproof is completed by applying H0.

Let x2 of type ι → ι → ο be given.

Assume H3: x2 (4ae4a.. x0) (4ae4a.. x0).

The subproof is completed by applying H3.

■

Proofgold Proof