Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: x03.
Let x1 of type ι be given.
Assume H1: x13.
Assume H2: 0x0 = 0x1.
Assume H3: 1x0 = 1x1.
Assume H4: 2x0 = 2x1.
Apply set_ext with x0, x1 leaving 2 subgoals.
Let x2 of type ι be given.
Assume H5: x2x0.
Apply cases_3 with x2, λ x3 . x3x0x3x1 leaving 5 subgoals.
Apply H0 with x2.
The subproof is completed by applying H5.
Apply H2 with λ x3 x4 : ο . x40x1.
Assume H6: 0x1.
The subproof is completed by applying H6.
Apply H3 with λ x3 x4 : ο . x41x1.
Assume H6: 1x1.
The subproof is completed by applying H6.
Apply H4 with λ x3 x4 : ο . x42x1.
Assume H6: 2x1.
The subproof is completed by applying H6.
The subproof is completed by applying H5.
Let x2 of type ι be given.
Assume H5: x2x1.
Apply cases_3 with x2, λ x3 . x3x1x3x0 leaving 5 subgoals.
Apply H1 with x2.
The subproof is completed by applying H5.
Apply H2 with λ x3 x4 : ο . 0x1x4.
Assume H6: 0x1.
The subproof is completed by applying H6.
Apply H3 with λ x3 x4 : ο . 1x1x4.
Assume H6: 1x1.
The subproof is completed by applying H6.
Apply H4 with λ x3 x4 : ο . 2x1x4.
Assume H6: 2x1.
The subproof is completed by applying H6.
The subproof is completed by applying H5.