Search for blocks/addresses/...

Proofgold Proof

pf
Apply unknownprop_f4ee121fb14a7412699d1f11bebf17d33e1718030f72ebf91211f8d97c32541d with λ x0 . prim3 (4ae4a.. x0) = x0.
Let x0 of type ι be given.
Assume H0: ba9d8.. x0.
Assume H1: ∀ x1 . prim1 x1 x0 ⟶ prim3 (4ae4a.. x1) = x1.
Apply set_ext with prim3 (4ae4a.. x0), x0 leaving 2 subgoals.
Let x1 of type ι be given.
Assume H2: prim1 x1 (prim3 (4ae4a.. x0)).
Apply UnionE_impred with 4ae4a.. x0, x1, prim1 x1 x0 leaving 2 subgoals.
The subproof is completed by applying H2.
Let x2 of type ι be given.
Assume H3: prim1 x1 x2.
Assume H4: prim1 x2 (4ae4a.. x0).
Apply unknownprop_45a165aaf9186993c6406ffae995383c566dba64cecdf4ad2d6396af4c93b1e4 with x0, x2, x1 leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H4.
The subproof is completed by applying H3.
Let x1 of type ι be given.
Assume H2: prim1 x1 x0.
Apply UnionI with 4ae4a.. x0, x1, x0 leaving 2 subgoals.
The subproof is completed by applying H2.
The subproof is completed by applying unknownprop_38ce50d6b52a0a920b530e7796207ec902a42d65414467df1ecd3efb123f4cb9 with x0.
■