no goals
α : Type u
α' : Type ?u.68385
β : Type v
β' : Type ?u.68390
γ : Type ?u.68393
φ : Type ?u.68396
inst✝⁵ : OmegaCompletePartialOrder α
inst✝⁴ : OmegaCompletePartialOrder β
inst✝³ : OmegaCompletePartialOrder γ
inst✝² : OmegaCompletePartialOrder φ
inst✝¹ : OmegaCompletePartialOrder α'
inst✝ : OmegaCompletePartialOrder β'
c₀ : Chain (α →𝒄 β)
c₁ : Chain α
z : β
⊢ (∀ (j i : ℕ), ↑(↑c₀ i).toOrderHom (↑c₁ j) ≤ z) ↔ ∀ (i : ℕ), ↑(↑c₀ i).toOrderHom (↑c₁ i) ≤ z
rw [forall_swap, forall_forall_merge]