Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι → ι be given.
Assume H0:
∀ x3 . x3 ∈ x0 ⟶ equip (x2 x3) x1.
Assume H1: ∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x2 x3 ⟶ x5 ∈ x2 x4 ⟶ x3 = x4.
Apply equip_tra with
famunion x0 (λ x3 . x2 x3),
lam x0 (λ x3 . x2 x3),
setprod x0 x1 leaving 2 subgoals.
Apply equip_sym with
lam x0 x2,
famunion x0 x2.
Apply unknownprop_049aa024f23bec37895017ca5d0e6546c46a1d5549f875fd117032f8f8ce9923 with
x0,
x2.
The subproof is completed by applying H1.
Apply unknownprop_ca35929bb9516758ce3c56c5bf7b9f0713e81693444871247a9d2c8c2835f309 with
x0,
x1,
x2.
The subproof is completed by applying H0.