Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Let x1 of type ι be given.
Apply prop_ext_2 with Subq x0 x1, binunion x0 x1 = x1 leaving 2 subgoals.
Assume H0: Subq x0 x1.
Apply unknownprop_a23ec6a55ac212526d74cbf0d04096929ad453b0eb0f8023e32b8a33930d39fb with binunion x0 x1, x1 leaving 2 subgoals.
Apply unknownprop_fb26fe958e64ebbf533947db0048c8f1c2bfe1ee93c5358b327221e99f81f109 with x0, x1, x1 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying unknownprop_d889823a5c975ad2d68f484964233a1e69e7d67f0888aa5b83d962eeca107acd with x1.
The subproof is completed by applying unknownprop_797168717b55ee5eded5eab45e11f1513074138c4f7a9fa70fbdac8b84ce4a03 with x0, x1.
Assume H0: binunion x0 x1 = x1.
Apply H0 with λ x2 x3 . Subq x0 x2.
The subproof is completed by applying unknownprop_45cad3d16e6a052331516a33ff7f695a27568e6c7992c9bc7ae67399a451422e with x0, x1.