Let x0 of type ι be given.

Let x1 of type ι be given.

Apply unknownprop_8e9afa6cbe34c70175f6c4dbdd044465af8aeced2be56c04dd43afb3a9abc68a with x0, 4a7ef.., x1, x1 = x0 leaving 4 subgoals.

The subproof is completed by applying unknownprop_e5c1596f5fd6bc2d713145a4e9d44688423a48751f219f9d9d142effb814941e.

The subproof is completed by applying H0.

Assume H1: and (4a7ef.. = 4a7ef..) (x1 = x0).

Apply H1 with x1 = x0.

Assume H2: 4a7ef.. = 4a7ef...

Assume H3: x1 = x0.

The subproof is completed by applying H3.

Assume H1: ∃ x2 x3 . and (and (4a7ef.. = 4ae4a.. x2) (x1 = prim3 x3)) (aa8d2.. x2 x0 x3).

Apply H1 with x1 = x0.

Let x2 of type ι be given.

Assume H2: (λ x3 . ∃ x4 . and (and (4a7ef.. = 4ae4a.. x3) (x1 = prim3 x4)) (aa8d2.. x3 x0 x4)) x2.

Apply H2 with x1 = x0.

Let x3 of type ι be given.

Assume H3: (λ x4 . and (and (4a7ef.. = 4ae4a.. x2) (x1 = prim3 x4)) (aa8d2.. x2 x0 x4)) x3.

Apply H3 with x1 = x0.

Assume H4: and (4a7ef.. = 4ae4a.. x2) (x1 = prim3 x3).

Apply H4 with aa8d2.. x2 x0 x3 ⟶ x1 = x0.

Assume H5: 4a7ef.. = 4ae4a.. x2.

Apply FalseE with x1 = prim3 x3 ⟶ aa8d2.. x2 x0 x3 ⟶ x1 = x0.

Apply unknownprop_e673ffa43d637e4ad1597cb67f33a29ca918f2b4d1035a90a508f3118c8fa9a3 with x2.

The subproof is completed by applying H5.

■

Proofgold Proof