We divide the binary fundamental lemma for Fμ,ref,par into several lemmas.
This also generalizes the lemmas. We used to show

Δ ∥ Γ ⊩ e ≤log≤ e ∷ τ

in the fundamental lemma. But now in smaller lemmas in each case we show

Δ ∥ Γ ⊩ e ≤log≤ e' ∷ τ

Given some hypotheses of course.