∀ {α : Type u_1} {R : α → α → Prop} {v : α} (head : α) (tail : List α),
  List.IsChain R (head :: tail) →
    (∀ (lne : head :: tail ≠ []), R v ((head :: tail).head lne)) → List.IsChain R (v :: head :: tail)