Using the idea we talked about offline, I was able to fix the proof—thanks Rohin! Summary of the fix: When D1 and D2 are defined, additionally assume they are biextensional (take their biextensional collapse), which is fine since we are trying to prove a biextensional equivalence. (By the way this is why we can’t take b1=b2, since we might have A⊇B1≠B2⊆A after biextensional collapse.) Then to prove h=hf1, observe that for all b∈B1, b∙1h(b′2)=b∙1h(b2) which means b⋆1h(b′2)=b⋆1f1, hence h(b′2)=f1 since a biextensional frame has no duplicate columns.
Using the idea we talked about offline, I was able to fix the proof—thanks Rohin!
Summary of the fix:
When D1 and D2 are defined, additionally assume they are biextensional (take their biextensional collapse), which is fine since we are trying to prove a biextensional equivalence. (By the way this is why we can’t take b1=b2, since we might have A⊇B1≠B2⊆A after biextensional collapse.) Then to prove h=hf1, observe that for all b∈B1, b∙1h(b′2)=b∙1h(b2) which means b⋆1h(b′2)=b⋆1f1, hence h(b′2)=f1 since a biextensional frame has no duplicate columns.