Search for blocks/addresses/...

Proofgold Proof

pf
Assume H0: TransSet (Sing 1).
Claim L1: 0Sing 1
Apply H0 with 1, 0 leaving 2 subgoals.
The subproof is completed by applying SingI with 1.
The subproof is completed by applying In_0_1.
Apply neq_0_1.
Apply SingE with 1, 0.
The subproof is completed by applying L1.