no goals
m n : ℕ
α : Fin (n + 1) → Type u
x✝ : α 0
q✝ : (i : Fin (n + 1)) → α i
p✝ : (i : Fin n) → α (succ i)
i : Fin n
y : α (succ i)
z : α 0
inst✝ : (i : Fin (n + 1)) → Preorder (α i)
x : α 0
q : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (succ i)
j : Fin n
⊢ q (succ j) ≤ cons x p (succ j) ↔ tail q j ≤ p j
simp [tail]