Proposition unary_interpolation_cofinal {i₁ i₂ : D} (q : D i₁ ⊑ D i₂) (j₁ : D_a i₁) : ∃ (j₂ : D_a i₂), D_a i₁ j₁ ⊑ D_a i₂ j₂. Proof. use (unary_interpolation_cofinal_lem q j₁ (D_a i₂)). apply refl_dcpo. Qed.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.OrderTheory.DCPOs.Core.DirectedSets. Require Import UniMath.OrderTheory.DCPOs.Core.Basics. Require Import UniMath.OrderTheory.DCPOs.Core.WayBelow.