Let x0 of type ι be given.

Let x1 of type ι be given.

Let x2 of type ι be given.

Assume H0: 762f0.. x0 x1 x2.

Apply H0 with λ x3 x4 x5 . and (and (e05e6.. x3) (74e69.. x4)) (74e69.. x5) leaving 9 subgoals.

Let x3 of type ι be given.

Assume H1: 74e69.. x3.

Apply and3I with e05e6.. c4def.., 74e69.. x3, 74e69.. x3 leaving 3 subgoals.

The subproof is completed by applying unknownprop_a866da150736a63955bc6564d827f7c01bae2a20c456de9663c4ff93bd67f424.

The subproof is completed by applying H1.

Let x3 of type ι be given.

Let x4 of type ι be given.

Let x5 of type ι be given.

Let x6 of type ι be given.

Let x7 of type ι be given.

Assume H1: (λ x8 x9 x10 . and (and (e05e6.. x8) (74e69.. x9)) (74e69.. x10)) x6 x3 x4.

Assume H2: (λ x8 x9 x10 . and (and (e05e6.. x8) (74e69.. x9)) (74e69.. x10)) x7 x4 x5.

Apply H1 with (λ x8 x9 x10 . and (and (e05e6.. x8) (74e69.. x9)) (74e69.. x10)) (6b90c.. x6 x7) x3 x5.

Assume H3: and (e05e6.. x6) (74e69.. x3).

Apply H3 with 74e69.. x4 ⟶ (λ x8 x9 x10 . and (and (e05e6.. x8) (74e69.. x9)) (74e69.. x10)) (6b90c.. x6 x7) x3 x5.

Assume H4: e05e6.. x6.

Assume H5: 74e69.. x3.

Assume H6: 74e69.. x4.

Apply H2 with (λ x8 x9 x10 . and (and (e05e6.. x8) (74e69.. x9)) (74e69.. x10)) (6b90c.. x6 x7) x3 x5.

Assume H7: and (e05e6.. x7) (74e69.. x4).

Apply H7 with 74e69.. x5 ⟶ (λ x8 x9 x10 . and (and (e05e6.. x8) (74e69.. x9)) (74e69.. x10)) (6b90c.. x6 x7) x3 x5.

Assume H8: e05e6.. x7.

Assume H9: 74e69.. x4.

Assume H10: 74e69.. x5.

Apply and3I with e05e6.. (6b90c.. x6 x7), 74e69.. x3, 74e69.. x5 leaving 3 subgoals.

Apply unknownprop_4848f0c516f3dfdf81cbeb2b0dd36b3edda90b804e511455f2dcb1cc0abd839b with x6, x7 leaving 2 subgoals.

The subproof is completed by applying H4.

The subproof is completed by applying H8.

The subproof is completed by applying H5.

The subproof is completed by applying H10.

Let x3 of type ι be given.

Assume H1: 74e69.. x3.

Apply and3I with e05e6.. c9248.., 74e69.. x3, 74e69.. 5e331.. leaving 3 subgoals.

The subproof is completed by applying unknownprop_838f5a3465e26bc783aad33e7deabf7fd0ebc2d8d0ca525057b427817f33cdce.

The subproof is completed by applying H1.

The subproof is completed by applying unknownprop_2889540f2161c9537dc388d6c2702e3891e2b8722a023eec016fa2e08ac47609.

Let x3 of type ι be given.

Let x4 of type ι be given.

Let x5 of type ι be given.

Let x6 of type ι be given.

Assume H1: 74e69.. x5.

Assume H2: (λ x7 x8 x9 . and (and (e05e6.. x7) (74e69.. x8)) (74e69.. x9)) x6 x3 x4.

Apply H2 with (λ x7 x8 x9 . and (and (e05e6.. x7) (74e69.. x8)) (74e69.. x9)) (a6e19.. x6) x3 (a3eb9.. x4 x5).

Assume H3: and (e05e6.. x6) (74e69.. x3).

Apply H3 with 74e69.. x4 ⟶ (λ x7 x8 x9 . and (and (e05e6.. x7) (74e69.. x8)) (74e69.. x9)) (a6e19.. x6) x3 (a3eb9.. x4 x5).

Assume H4: e05e6.. x6.

Assume H5: 74e69.. x3.

Assume H6: 74e69.. x4.

Apply and3I with e05e6.. (a6e19.. x6), 74e69.. x3, 74e69.. (a3eb9.. x4 x5) leaving 3 subgoals.

Apply unknownprop_4c282b9faa87cf98ec755257bbb7d88a24943ff260debf59b7c422310bade2ae with x6.

The subproof is completed by applying H4.

The subproof is completed by applying H5.

Apply unknownprop_7b384c9f4f31c662ca4b7cd8d8994d6b48c2b0c98a439c0ee694578d2722b3a7 with x4, x5 leaving 2 subgoals.

The subproof is completed by applying H6.

The subproof is completed by applying H1.

Let x3 of type ι be given.

Let x4 of type ι be given.

Let x5 of type ι be given.

Let x6 of type ι be given.

Assume H1: 74e69.. ....

...

■

Proofgold Proof