this : ?m.385414
⊢ Primrec' fun v => Vector.head v - Vector.head (Vector.tail v)

case this

⊢ ?m.385414
⊢ Primrec' fun v => Vector.head v - Vector.head (Vector.tail v)
suffices
case this

⊢ Primrec' fun v => (fun a b => b - a) (Vector.head v) (Vector.head (Vector.tail v))
this : ?m.385414
⊢ Primrec' fun v => Vector.head v - Vector.head (Vector.tail v)

case this

⊢ ?m.385414
simpa using comp₂ (fun a b => b - a) this (tail head) head
case this
v : Vector ℕ (Nat.succ 0 + 1)
⊢ Nat.rec (Vector.head (Vector.tail v)) (fun y IH => Nat.pred (Vector.head (Vector.tail (y ::ᵥ IH ::ᵥ Vector.tail v))))
      (Vector.head v) =
    (fun a b => b - a) (Vector.head v) (Vector.head (Vector.tail v))
case this

⊢ Primrec' fun v => (fun a b => b - a) (Vector.head v) (Vector.head (Vector.tail v))
refine' (prec head (pred.comp₁ _ (tail head))).of_eq fun v => _
case this
v : Vector ℕ (Nat.succ 0 + 1)
⊢ Nat.rec (Vector.head (Vector.tail v)) (fun y IH => Nat.pred IH) (Vector.head v) =
    Vector.head (Vector.tail v) - Vector.head v
case this
v : Vector ℕ (Nat.succ 0 + 1)
⊢ Nat.rec (Vector.head (Vector.tail v)) (fun y IH => Nat.pred (Vector.head (Vector.tail (y ::ᵥ IH ::ᵥ Vector.tail v))))
      (Vector.head v) =
    (fun a b => b - a) (Vector.head v) (Vector.head (Vector.tail v))
simp
no goals
case this
v : Vector ℕ (Nat.succ 0 + 1)
⊢ Nat.rec (Vector.head (Vector.tail v)) (fun y IH => Nat.pred IH) (Vector.head v) =
    Vector.head (Vector.tail v) - Vector.head v
induction v.head <;> simp [*, Nat.sub_succ]