Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Let x1 of type ι be given.
Assume H0: 80242.. x0.
Assume H1: 80242.. x1.
Assume H2: fe4bb.. x0 x1.
Apply unknownprop_144f26d28c36e53fd447ba70115cd55d32e895160d4fb202367d3cd577066d73 with x0, x1, fe4bb.. (f4dc0.. x1) (f4dc0.. x0) leaving 5 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
Assume H3: 099f3.. x0 x1.
Apply unknownprop_3bb88212dd853920577537bc3ecbc5e3e2bf8309e1e59246b79ae30400fc333e with f4dc0.. x1, f4dc0.. x0.
Apply unknownprop_3cc82c9758d3882690e6647e4154486613d1a5c615c0651627364410273ab026 with x0, x1 leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying H3.
Assume H3: x0 = x1.
Apply H3 with λ x2 x3 . fe4bb.. (f4dc0.. x1) (f4dc0.. x3).
The subproof is completed by applying unknownprop_f017f6ee910dd235f4bf08afbbbf148d42e1360d8b1094fb435baedbfe8b2ac8 with f4dc0.. x1.