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: x1 x2.
Assume H2: x1 x3.
Let x4 of type ι → ι → ο be given.
Apply CD_proj1_1 with
x0,
x1,
pair_tag x0 x2 x3,
x3 = CD_proj1 x0 x1 (pair_tag x0 x2 x3),
λ x5 x6 . x4 x6 x5 leaving 3 subgoals.
The subproof is completed by applying H0.
Apply CD_carr_I with
x0,
x1,
x2,
x3 leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
Apply CD_proj0_2 with
x0,
x1,
x2,
x3,
λ x5 x6 . pair_tag x0 x2 x3 = pair_tag x0 x6 (CD_proj1 x0 x1 (pair_tag x0 x2 x3)) ⟶ x3 = CD_proj1 x0 x1 (pair_tag x0 x2 x3) leaving 4 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
Apply pair_tag_prop_2 with
x0,
x1,
x2,
x3,
x2,
CD_proj1 x0 x1 (pair_tag x0 x2 x3) leaving 6 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
The subproof is completed by applying H1.
The subproof is completed by applying H3.
The subproof is completed by applying H4.