Search for blocks/addresses/...

Proofgold Proof

pf
Apply In_ind with λ x0 . ∀ x1 . x0x1x1x0False.
Let x0 of type ι be given.
Assume H0: ∀ x1 . x1x0∀ x2 . x1x2x2x1False.
Let x1 of type ι be given.
Assume H1: x0x1.
Assume H2: x1x0.
Apply H0 with x1, x0 leaving 3 subgoals.
The subproof is completed by applying H2.
The subproof is completed by applying H2.
The subproof is completed by applying H1.