converges: ∀q1,q2.
(Ext⎽bp q1 ∧ (Ext⎽bp q2)) = (Ext⎽bp ((downarrow q1) ∧ (downarrow q2)));
all_covered: Ext⎽bp (oa_one (form bp)) = oa_one (concr bp);
- il2: ∀I:setoid.∀p:ums I (oa_P (form bp)).
+ il2: ∀I:SET.∀p:arrows1 SET I (oa_P (form bp)).
downarrow (oa_join ? I (d_p_i ?? downarrow p)) =
oa_join ? I (d_p_i ?? downarrow p);
il1: ∀q.downarrow (A ? q) = A ? q