Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Apply set_ext with prim3 x0, a842e.. x0 (λ x1 . x1) leaving 2 subgoals.
Let x1 of type ι be given.
Assume H0: prim1 x1 (prim3 x0).
Apply UnionE_impred with x0, x1, prim1 x1 (a842e.. x0 (λ x2 . x2)) leaving 2 subgoals.
The subproof is completed by applying H0.
Let x2 of type ι be given.
Assume H1: prim1 x1 x2.
Assume H2: prim1 x2 x0.
Apply unknownprop_1a58846f991745a62bb791e57f6ffb9f18f2ca362367c10b2b979fc90a3b62e1 with x0, λ x3 . x3, x2, x1 leaving 2 subgoals.
The subproof is completed by applying H2.
The subproof is completed by applying H1.
Let x1 of type ι be given.
Assume H0: prim1 x1 (a842e.. x0 (λ x2 . x2)).
Apply unknownprop_6e713ef2b1c9d2089dead8e3d98fed6bda91ffc6b807ed8732c89724a15f5c2c with x0, λ x2 . x2, x1, prim1 x1 (prim3 x0) leaving 2 subgoals.
The subproof is completed by applying H0.
Let x2 of type ι be given.
Assume H1: and (prim1 x2 x0) (prim1 x1 x2).
Apply H1 with prim1 x1 (prim3 x0).
Assume H2: prim1 x2 x0.
Assume H3: prim1 x1 x2.
Apply UnionI with x0, x1, x2 leaving 2 subgoals.
The subproof is completed by applying H3.
The subproof is completed by applying H2.
■