Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: SNo x0.
Apply mul_SNo_distrL with eps_ 1, x0, x0, λ x1 x2 . x0 = x2 leaving 4 subgoals.
Apply SNo_eps_ with 1.
Apply nat_p_omega with 1.
The subproof is completed by applying nat_1.
The subproof is completed by applying H0.
The subproof is completed by applying H0.
Let x1 of type ιιο be given.
Apply eps_1_split_eq with x0, λ x2 x3 . x1 x3 x2.
The subproof is completed by applying H0.