- [ lapply (sor_comm_23 … Hg0 Hg1 ?) -g0 [3: |*: // ] #Hg1
- /3 width=11 by lsubf_push, lsubf_beta, sor_np, ex3_2_intro/
- | lapply (sor_assoc_dx … Hg1 … Hg0 ??) -g0 [3: |*: // ] #Hg1
- /3 width=11 by lsubf_push, lsubf_beta, sor_pn, ex3_2_intro/
- | lapply (sor_distr_dx … Hg0 … Hg1) -g0 [5: |*: // ] #Hg1
- /3 width=11 by lsubf_beta, sor_nn, ex3_2_intro/
+ [ lapply (pr_sor_comm_23 … Hg0 Hg1 ?) -g0 [3: |*: // ] #Hg1
+ /3 width=11 by lsubf_push, lsubf_beta, pr_sor_next_push, ex3_2_intro/
+ | lapply (pr_sor_assoc_dx … Hg1 … Hg0 ??) -g0 [3: |*: // ] #Hg1
+ /3 width=11 by lsubf_push, lsubf_beta, pr_sor_push_next, ex3_2_intro/
+ | lapply (pr_sor_distr_dx … Hg0 … Hg1) -g0 [5: |*: // ] #Hg1
+ /3 width=11 by lsubf_beta, pr_sor_next_bi, ex3_2_intro/