∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [inst : MetricSpace X] [inst_1 : MetricSpace Y] [Nonempty Z] (Φ : Z → X)
  (Ψ : Z → Y) (ε : ℝ),
  (∀ (p q : Z), |dist (Φ p) (Φ q) - dist (Ψ p) (Ψ q)| ≤ 2 * ε) → ∀ (x y : X ⊕ Y), 0 ≤ Metric.glueDist Φ Ψ ε x y