- elim (sor_inv_pnx … Hf) -Hf [1,6,11,16:|*: // ] #x #Hx #H destruct
- /3 width=12 by lsubf_unit, lsubf_beta, lsubf_bind, sor_assoc_sn/
- | elim (sor_inv_npx … Hg) -Hg [|*: // ] #y #Hy #H destruct
+ elim (pr_sor_inv_push_next … Hf) -Hf [1,6,11,16:|*: // ] #x #Hx #H destruct
+ /3 width=12 by lsubf_unit, lsubf_beta, lsubf_bind, pr_sor_assoc_sn/
+ | elim (pr_sor_inv_next_push … Hg) -Hg [|*: // ] #y #Hy #H destruct