Let x0 of type ι → ο be given.
Let x1 of type ι be given.
Let x2 of type ι be given.
Let x3 of type ι be given.
Assume H1: x0 x1.
Assume H2: x0 x2.
Apply H0 with
x1,
λ x4 . Hom_b_b_r_e_e x4 x2 x3 ⟶ x3 ∈ setexp (ap x2 0) (ap x4 0) leaving 2 subgoals.
The subproof is completed by applying H1.
Let x4 of type ι be given.
Let x5 of type ι → ι → ι be given.
Assume H3: ∀ x6 . x6 ∈ x4 ⟶ ∀ x7 . x7 ∈ x4 ⟶ x5 x6 x7 ∈ x4.
Let x6 of type ι → ι → ι be given.
Assume H4: ∀ x7 . x7 ∈ x4 ⟶ ∀ x8 . x8 ∈ x4 ⟶ x6 x7 x8 ∈ x4.
Let x7 of type ι → ι → ο be given.
Let x8 of type ι be given.
Assume H5: x8 ∈ x4.
Let x9 of type ι be given.
Assume H6: x9 ∈ x4.
Apply H0 with
x2,
λ x10 . Hom_b_b_r_e_e (pack_b_b_r_e_e x4 x5 x6 x7 x8 x9) x10 x3 ⟶ x3 ∈ setexp (ap x10 0) (ap (pack_b_b_r_e_e x4 x5 x6 x7 x8 x9) 0) leaving 2 subgoals.
The subproof is completed by applying H2.
Let x10 of type ι be given.
Let x11 of type ι → ι → ι be given.
Assume H7: ∀ x12 . x12 ∈ x10 ⟶ ∀ x13 . x13 ∈ x10 ⟶ x11 x12 x13 ∈ x10.
Let x12 of type ι → ι → ι be given.
Assume H8: ∀ x13 . x13 ∈ x10 ⟶ ∀ x14 . x14 ∈ x10 ⟶ x12 x13 x14 ∈ x10.
Let x13 of type ι → ι → ο be given.
Let x14 of type ι be given.
Assume H9: x14 ∈ x10.
Let x15 of type ι be given.
Assume H10: x15 ∈ x10.
Apply unknownprop_3b7da8c0bd80210288926533162c56f13aa350f06168ea4a8789f8cd5ca03194 with
x4,
x10,
x5,
x6,
x11,
x12,
x7,
x13,
x8,
x9,
x14,
x15,
x3,
λ x16 x17 : ο . x17 ⟶ x3 ∈ setexp (ap (pack_b_b_r_e_e x10 x11 x12 x13 x14 x15) 0) (ap (pack_b_b_r_e_e x4 x5 x6 x7 x8 x9) 0).
Assume H11:
and (and (and (and (and (x3 ∈ setexp x10 x4) (∀ x16 . x16 ∈ x4 ⟶ ∀ x17 . x17 ∈ x4 ⟶ ap x3 (x5 x16 x17) = x11 (ap x3 x16) (ap x3 x17))) (∀ x16 . x16 ∈ x4 ⟶ ∀ x17 . x17 ∈ x4 ⟶ ap x3 (x6 x16 x17) = x12 (ap x3 x16) (ap x3 x17))) (∀ x16 . x16 ∈ x4 ⟶ ∀ x17 . x17 ∈ x4 ⟶ x7 x16 x17 ⟶ x13 (ap x3 x16) (ap x3 x17))) (ap x3 x8 = x14)) (ap x3 x9 = x15).
Apply pack_b_b_r_e_e_0_eq2 with
x10,
x11,
x12,
x13,
x14,
...,
....
Apply unknownprop_cb7abf829499aec888363ff9292dd7680786c42dc92f10fdd88dc16ada048723 with
x0,
λ x1 . ap x1 0,
Hom_b_b_r_e_e.
The subproof is completed by applying L1.