Let x0 of type ι be given.

Let x1 of type ι → ο be given.

Assume H0: ∀ x2 . x1 x2 ⟶ ∀ x3 . x3 ∈ x2 ⟶ nIn x0 x3.

Let x2 of type ι be given.

Let x3 of type ι be given.

Assume H1: CD_carr x0 x1 x2.

Assume H2: CD_carr x0 x1 x3.

Assume H3: CD_proj0 x0 x1 x2 = CD_proj0 x0 x1 x3.

Assume H4: CD_proj1 x0 x1 x2 = CD_proj1 x0 x1 x3.

set y4 to be x2

set y5 to be y4

Claim L5: ∀ x6 : ι → ο . x6 y5 ⟶ x6 y4

Let x6 of type ι → ο be given.

Assume H5: x6 y5.

Apply CD_proj0proj1_eta with x2, x3, y4, λ x7 . x6 leaving 3 subgoals.

The subproof is completed by applying H0.

The subproof is completed by applying H1.

set y7 to be pair_tag x2 (CD_proj0 x2 x3 y4) (CD_proj1 x2 x3 y4)

set y8 to be x6

Claim L6: ∀ x9 : ι → ο . x9 y8 ⟶ x9 y7

Let x9 of type ι → ο be given.

Assume H6: x9 y7.

Apply H3 with λ x10 x11 . pair_tag y4 x11 (CD_proj1 y4 y5 x6) = pair_tag y4 (CD_proj0 y4 y5 y7) (CD_proj1 y4 y5 y7), λ x10 . x9 leaving 2 subgoals.

Apply H4 with λ x10 x11 . pair_tag y4 (CD_proj0 y4 y5 y7) x11 = pair_tag y4 (CD_proj0 y4 y5 y7) (CD_proj1 y4 y5 y7).

Let x10 of type ι → ι → ο be given.

Assume H7: x10 (pair_tag y4 (CD_proj0 y4 y5 y7) (CD_proj1 y4 y5 y7)) (pair_tag y4 (CD_proj0 y4 y5 y7) (CD_proj1 y4 y5 y7)).

The subproof is completed by applying H7.

set y10 to be λ x10 . x9

Apply CD_proj0proj1_eta with y4, y5, y7, λ x11 x12 . y10 x12 x11 leaving 3 subgoals.

The subproof is completed by applying H0.

The subproof is completed by applying H2.

The subproof is completed by applying H6.

set y9 to be λ x9 . y8

Apply L6 with λ x10 . y9 x10 y8 ⟶ y9 y8 x10 leaving 2 subgoals.

Assume H7: y9 y8 y8.

The subproof is completed by applying H7.

The subproof is completed by applying L6.

Let x6 of type ι → ι → ο be given.

Apply L5 with λ x7 . x6 x7 y5 ⟶ x6 y5 x7.

Assume H6: x6 y5 y5.

The subproof is completed by applying H6.

■

Proofgold Proof