Let x0 of type ι be given.
Apply H0 with
struct_b_b_e_e x0.
Assume H2:
unpack_b_b_e_e_o x0 (λ x1 . λ x2 x3 : ι → ι → ι . λ x4 x5 . and (and (and (and (and (and (and (and (∀ x6 . x6 ∈ x1 ⟶ ∀ x7 . x7 ∈ x1 ⟶ ∀ x8 . x8 ∈ x1 ⟶ x2 (x2 x6 x7) x8 = x2 x6 (x2 x7 x8)) (∀ x6 . x6 ∈ x1 ⟶ ∀ x7 . x7 ∈ x1 ⟶ x2 x6 x7 = x2 x7 x6)) (∀ x6 . x6 ∈ x1 ⟶ x2 x6 x4 = x6)) (∀ x6 . x6 ∈ x1 ⟶ ∀ x7 . x7 ∈ x1 ⟶ ∀ x8 . x8 ∈ x1 ⟶ x3 (x3 x6 x7) x8 = x3 x6 (x3 x7 x8))) (∀ x6 . x6 ∈ x1 ⟶ and (x3 x6 x5 = x6) (x3 x5 x6 = x6))) (∀ x6 . x6 ∈ x1 ⟶ ∀ x7 . x7 ∈ x1 ⟶ ∀ x8 . x8 ∈ x1 ⟶ x3 x6 (x2 x7 x8) = x2 (x3 x6 x7) (x3 x6 x8))) (∀ x6 . x6 ∈ x1 ⟶ ∀ x7 . x7 ∈ x1 ⟶ ∀ x8 . x8 ∈ x1 ⟶ x3 (x2 x6 x7) x8 = x2 (x3 x6 x8) (x3 x7 x8))) (∀ x6 . x6 ∈ x1 ⟶ x3 x6 x4 = x4)) (∀ x6 . x6 ∈ x1 ⟶ x3 x4 x6 = x4)).
The subproof is completed by applying H1.
Apply unknownprop_45b4495cd670852170dc3fe96ab30b08a69267996b7bee43e50ace860cabc334 with
Rig.
The subproof is completed by applying L0.