Search for blocks/addresses/...

Proofgold Proof

pf
Apply conj_HSNo_conj_CSNo with 0, λ x0 x1 . x1 = 0 leaving 2 subgoals. The subproof is completed by applying CSNo_0. The subproof is completed by applying conj_CSNo_0. ■