no goals
α : Type u_1
n : ℕ
r : α → α → Prop
inst✝ : IsTrans α r
f : Fin (n + 1) → α
a : α
⊢ ((fun x x_1 => x < x_1) ⇒ r) (vecCons a f) (vecCons a f) ↔ r a (f 0) ∧ ((fun x x_1 => x < x_1) ⇒ r) f f
simp only [liftFun_iff_succ r, forall_fin_succ, cons_val_succ, cons_val_zero, ← succ_castSucc,
  castSucc_zero]