proof(ordinal): unbudgeted sound-carrier extended order wf-<ᵇ⁺² (K-limited shared-binder)

proof(ordinal): unbudgeted sound-carrier extended order wf-<ᵇ⁺² (K-limited shared-binder) #82