This isn’t true, because ∙1 doesn’t just ignore b1 here (since r∈R1). I think the route is to say “Let h(b′2)=f2 . Then ∙1 must treat f1 and f2 identically, meaning that either they are equal, or the frame is biextensionally equivalent to one where they are equal.”
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.
The problem is a bit earlier actually:
This isn’t true, because ∙1 doesn’t just ignore b1 here (since r∈R1). I think the route is to say “Let h(b′2)=f2 . Then ∙1 must treat f1 and f2 identically, meaning that either they are equal, or the frame is biextensionally equivalent to one where they are equal.”
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.