Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: x0 ∈ u17.
Let x1 of type ι be given.
Assume H1: x1 ∈ u17.
Assume H2: 0aea9.. x0 x1.
Assume H3: x0 ∈ u17.
Assume H4: x1 ∈ u17.
Apply unknownprop_52ef8eab68e09c76e641a050138db31c7398e256ad409f424be6110e012b78a4 with x0, x1, λ x2 x3 : ι → ι → ι . x3 = λ x4 x5 . x4 leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
Apply H2 leaving 2 subgoals.
Apply unknownprop_f58cc828ea3d14d0814f62d53b092f625eabe356edf3964e5549d4f35f071dc8 with x0.
The subproof is completed by applying H0.
Apply unknownprop_f58cc828ea3d14d0814f62d53b092f625eabe356edf3964e5549d4f35f071dc8 with x1.
The subproof is completed by applying H1.
■