Let x0 of type ο be given.

Assume H0: ∀ x1 : ι → ι . (∃ x2 : ι → ι → ι → ι . ∃ x3 x4 : ι → ι . MetaAdjunction_strict (λ x5 . True) HomSet (λ x5 . lam_id x5) (λ x5 x6 x7 x8 x9 . lam_comp x5 x8 x9) IrreflexiveTransitiveReln BinRelnHom struct_id struct_comp x1 x2 (λ x5 . ap x5 0) (λ x5 x6 x7 . x7) x3 x4) ⟶ x0.

Apply H0 with λ x1 . pack_r x1 (λ x2 x3 . False).

Let x1 of type ο be given.

Assume H1: ∀ x2 : ι → ι → ι → ι . (∃ x3 x4 : ι → ι . MetaAdjunction_strict (λ x5 . True) HomSet (λ x5 . lam_id x5) (λ x5 x6 x7 x8 x9 . lam_comp x5 x8 x9) IrreflexiveTransitiveReln BinRelnHom struct_id struct_comp (λ x5 . pack_r x5 (λ x6 x7 . False)) x2 (λ x5 . ap x5 0) (λ x5 x6 x7 . x7) x3 x4) ⟶ x1.

Apply H1 with λ x2 x3 x4 . x4.

Let x2 of type ο be given.

Assume H2: ∀ x3 : ι → ι . (∃ x4 : ι → ι . MetaAdjunction_strict (λ x5 . True) HomSet (λ x5 . lam_id x5) (λ x5 x6 x7 x8 x9 . lam_comp x5 x8 x9) IrreflexiveTransitiveReln BinRelnHom struct_id struct_comp (λ x5 . pack_r x5 (λ x6 x7 . False)) (λ x5 x6 x7 . x7) (λ x5 . ap x5 0) (λ x5 x6 x7 . x7) x3 x4) ⟶ x2.

Apply H2 with λ x3 . lam_id x3.

Let x3 of type ο be given.

Assume H3: ∀ x4 : ι → ι . MetaAdjunction_strict (λ x5 . True) HomSet (λ x5 . lam_id x5) (λ x5 x6 x7 x8 x9 . lam_comp x5 x8 x9) IrreflexiveTransitiveReln BinRelnHom struct_id struct_comp (λ x5 . pack_r x5 (λ x6 x7 . False)) (λ x5 x6 x7 . x7) (λ x5 . ap x5 0) (λ x5 x6 x7 . x7) (λ x5 . lam_id x5) x4 ⟶ x3.

Apply H3 with λ x4 . lam_id (ap x4 0).

Claim L4: ...

...

Claim L5: ...

...

Claim L6: ...

...

Apply unknownprop_712520f713b96d5afd10321cea9a3c978868fc53aa35a29461e902d5b5a4ba79 with λ x4 . True, HomSet, λ x4 . lam_id x4, λ x4 x5 x6 x7 x8 . lam_comp x4 x7 x8, IrreflexiveTransitiveReln, BinRelnHom, struct_id, struct_comp, λ x4 . pack_r x4 (λ x5 x6 . False), λ x4 x5 x6 . x6, λ x4 . ap x4 0, λ x4 x5 x6 . x6, λ x4 . lam_id x4, λ x4 . lam_id (ap x4 0) leaving 5 subgoals.

Apply unknownprop_3d05796578cdc17ebd2096167db48ecef934256d250d1637eb5dd67225cdfe05 with λ x4 . True, HomSet, λ x4 . lam_id x4, λ x4 x5 x6 x7 x8 . lam_comp x4 x7 x8, IrreflexiveTransitiveReln, BinRelnHom, struct_id, struct_comp, λ x4 . pack_r x4 (λ x5 x6 . False), λ x4 x5 x6 . x6 leaving 3 subgoals.

The subproof is completed by applying unknownprop_dcf5739aa5fe0adc626fd983737b233fe68652dff14c53b3d75823dcf2542d41.

The subproof is completed by applying unknownprop_3cfb35338d6b874e5c5bd0760253f7ac65e99ffc814bd52eef4adff85a56dbe0.

Apply unknownprop_795e291855a044d4d636c961caa1600704603cc02e33a7b37aa66e8d7f6512db with λ x4 . True, HomSet, λ x4 . lam_id x4, λ x4 x5 x6 x7 x8 . lam_comp x4 x7 x8, IrreflexiveTransitiveReln, BinRelnHom, struct_id, struct_comp, λ x4 . pack_r x4 (λ x5 x6 . False), λ x4 x5 x6 . x6 leaving 4 subgoals.

Let x4 of type ι be given.

Assume H7: (λ x5 . True) x4.

Apply unknownprop_dbb6377af3127d2bf8cd888143d856b4a86f0ec975822a440e0313d91ee07474 with x4, λ x5 x6 . False leaving 2 subgoals.

Let x5 of type ι be given.

Assume H8: x5 ∈ x4.

Assume H9: False.

The subproof is completed by applying H9.

Let x5 of type ι be given.

Assume H8: x5 ∈ x4.

Let x6 of type ι be given.

Assume H9: x6 ∈ x4.

Let x7 of type ι be given.

Assume H10: x7 ∈ x4.

Assume H11: (λ x8 x9 . False) x5 x6.

Assume H12: (λ x8 x9 . False) x6 x7.

The subproof is completed by applying H11.

...

■

Proofgold Proof