[ apply (λo: basic_pair.λa,b: Ω \sup (form o).{c | BPext o c ⊆ BPextS o a ∩ BPextS o b });
intros; simplify; apply (.= (†e)‡#); apply refl1
| intros; split; simplify; intros;
[ apply (λo: basic_pair.λa,b: Ω \sup (form o).{c | BPext o c ⊆ BPextS o a ∩ BPextS o b });
intros; simplify; apply (.= (†e)‡#); apply refl1
| intros; split; simplify; intros;