napply (replace_char … { x | ϕ a x = O }); ##[##1,2: #x; nrewrite > (H x); //; ##]
napply (axiom_cond … a one); ##] #H1;
ncut (a ◃ ∅); ##[ napply (transitivity … H1); //; ##] #H2;
nlapply (col2_4 …H2); #H3;
ncut (a ∈ 𝐂 a one); ##[
napply (replace_char … { x | ϕ a x = O }); ##[##1,2: #x; nrewrite > (H x); //; ##]
napply (axiom_cond … a one); ##] #H1;
ncut (a ◃ ∅); ##[ napply (transitivity … H1); //; ##] #H2;
nlapply (col2_4 …H2); #H3;
ncut (a ∈ 𝐂 a one); ##[