Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ιι be given.
Assume H0: ∀ x3 . x3x0equip (x2 x3) x1.
Assume H1: ∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x2 x3x5x2 x4x3 = 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.