Let x0 of type ι be given.

Let x1 of type ι be given.

Assume H0: prim1 x0 x1.

Assume H1: prim1 x1 x0.

Apply unknownprop_c305b585b05bbd5dfb1f2334fba160b28fdb98c88197eae477bd0e829ec1b7cd with prim2 x0 x1, x0, False leaving 2 subgoals.

The subproof is completed by applying unknownprop_893870ab8a49d622c10a8fe954eea30d7bd2b94aa27e9c6b21eab85a9f81d115 with x0, x1.

Let x2 of type ι be given.

Assume H2: (λ x3 . and (prim1 x3 (prim2 x0 x1)) (not (∃ x4 . and (prim1 x4 (prim2 x0 x1)) (prim1 x4 x3)))) x2.

Apply H2 with False.

Assume H3: prim1 x2 (prim2 x0 x1).

Assume H4: not (∃ x3 . and (prim1 x3 (prim2 x0 x1)) (prim1 x3 x2)).

Apply unknownprop_44132e34b8fcc92e54ff875d0e8f6137eeea7d41bb9d4b117dbbbb4d2f239782 with x2, x0, x1, False leaving 3 subgoals.

The subproof is completed by applying H3.

Assume H5: x2 = x0.

Apply H4.

Let x3 of type ο be given.

Assume H6: ∀ x4 . and (prim1 x4 (prim2 x0 x1)) (prim1 x4 x2) ⟶ x3.

Apply H6 with x1.

Apply andI with prim1 x1 (prim2 x0 x1), prim1 x1 x2 leaving 2 subgoals.

The subproof is completed by applying unknownprop_70f06371245ce38fbbca963cb4d7e422ccf350d2e27735c617635b09cbcba701 with x0, x1.

Apply H5 with λ x4 x5 . prim1 x1 x5.

The subproof is completed by applying H1.

Assume H5: x2 = x1.

Apply H4.

Let x3 of type ο be given.

Assume H6: ∀ x4 . and (prim1 x4 (prim2 x0 x1)) (prim1 x4 x2) ⟶ x3.

Apply H6 with x0.

Apply andI with prim1 x0 (prim2 x0 x1), prim1 x0 x2 leaving 2 subgoals.

The subproof is completed by applying unknownprop_893870ab8a49d622c10a8fe954eea30d7bd2b94aa27e9c6b21eab85a9f81d115 with x0, x1.

Apply H5 with λ x4 x5 . prim1 x0 x5.

The subproof is completed by applying H0.

■

Proofgold Proof