Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: atleastp 3 x0.
Let x1 of type ο be given.
Assume H1: ∀ x2 . x2x0∀ x3 . x3x0∀ x4 . x4x0(x2 = x3∀ x5 : ο . x5)(x2 = x4∀ x5 : ο . x5)(x3 = x4∀ x5 : ο . x5)x1.
Apply H0 with x1.
Let x2 of type ιι be given.
Assume H2: inj 3 x0 x2.
Apply H2 with x1.
Assume H3: ∀ x3 . x33x2 x3x0.
Assume H4: ∀ x3 . x33∀ x4 . x43x2 x3 = x2 x4x3 = x4.
Apply H1 with x2 0, x2 1, x2 2 leaving 6 subgoals.
Apply H3 with 0.
The subproof is completed by applying In_0_3.
Apply H3 with 1.
The subproof is completed by applying In_1_3.
Apply H3 with 2.
The subproof is completed by applying In_2_3.
Assume H5: x2 0 = x2 1.
Apply neq_0_1.
Apply H4 with 0, 1 leaving 3 subgoals.
The subproof is completed by applying In_0_3.
The subproof is completed by applying In_1_3.
The subproof is completed by applying H5.
Assume H5: x2 0 = x2 2.
Apply neq_0_2.
Apply H4 with 0, 2 leaving 3 subgoals.
The subproof is completed by applying In_0_3.
The subproof is completed by applying In_2_3.
The subproof is completed by applying H5.
Assume H5: x2 1 = x2 2.
Apply neq_1_2.
Apply H4 with 1, 2 leaving 3 subgoals.
The subproof is completed by applying In_1_3.
The subproof is completed by applying In_2_3.
The subproof is completed by applying H5.