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) IrreflexiveSymmetricReln 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) IrreflexiveSymmetricReln 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) IrreflexiveSymmetricReln 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) IrreflexiveSymmetricReln 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, IrreflexiveSymmetricReln, 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, IrreflexiveSymmetricReln, 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_53ea818e2021d87ac705f8683274896fc426e94dc27b29259138e0d21bd2ebcf.

Apply unknownprop_795e291855a044d4d636c961caa1600704603cc02e33a7b37aa66e8d7f6512db with λ x4 . True, HomSet, λ x4 . lam_id x4, λ x4 x5 x6 x7 x8 . lam_comp x4 x7 x8, IrreflexiveSymmetricReln, 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_d442b731cc8a623579f119dd4140f334acbb8f35c49c35a487654154f8239ef6 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.

Assume H10: (λ x7 x8 . False) x5 x6.

The subproof is completed by applying H10.

Let x4 of type ι be given.

Let x5 of type ι be given.

Let x6 of type ι be given.

Assume H7: (λ x7 . True) x4.

...

■

Proofgold Proof