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:
∀ x4 . x4 ∈ x0 ⟶ equip (x3 x4) x2.
Assume H2: ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x3 x4 ⟶ x6 ∈ x3 x5 ⟶ x4 = x5.
Apply equip_tra with
famunion x0 (λ x4 . x3 x4),
setprod x0 x2,
setprod x1 x2 leaving 2 subgoals.
Apply unknownprop_541d2a46e6af37610d6dff1d2dff7b5d4d2a3850b13b6760afcea4d08ae0f05f with
x0,
x2,
x3 leaving 2 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
Apply unknownprop_114be8822b6413aaa4f094e79f9ed7dccf7f251af45e6784755c2493769eabfa with
x0,
x1,
x2,
x2 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying equip_ref with x2.