| ∀ x0 x1 . ∀ x2 x3 x4 x5 : ι → ι → ι . ∀ x6 x7 : ι → ι → ο . ∀ x8 x9 x10 x11 x12 . Hom_b_b_r_e_e (pack_b_b_r_e_e x0 x2 x3 x6 x8 x9) (pack_b_b_r_e_e x1 x4 x5 x7 x10 x11) x12 = and (and (and (and (and (x12 ∈ setexp x1 x0) (∀ x14 . x14 ∈ x0 ⟶ ∀ x15 . x15 ∈ x0 ⟶ ap x12 (x2 x14 x15) = x4 (ap x12 x14) (ap x12 x15))) (∀ x14 . x14 ∈ x0 ⟶ ∀ x15 . x15 ∈ x0 ⟶ ap x12 (x3 x14 x15) = x5 (ap x12 x14) (ap x12 x15))) (∀ x14 . x14 ∈ x0 ⟶ ∀ x15 . x15 ∈ x0 ⟶ x6 x14 x15 ⟶ x7 (ap x12 x14) (ap x12 x15))) (ap x12 x8 = x10)) (ap x12 x9 = x11) |
|