We want

   refine (
        let diag := (fun n : nat =>
 match n as n0 return (forall (v : vector n0) (_ : P n0 v), Type) with
 | O => fun (v : vector O) (_ : P O v) => forall _ : False, True
 | S x =>
     fun v : vector (S x) =>
     match
       v as w in (vector n0)
       return
         match n0 as n1 return (forall _ : vector n1, Type) with
         | O => fun _ : vector O => forall _ : False, True
         | S x0 => fun v0 : vector (S x0) => forall _ : P (S x0) v0, Type
         end w
     with
     | nil => fun H : False => False_rect True H
     | cons n0 x0 v0 => fun _ : P (S n0) (cons n0 x0 v0) => P n0 v0
     end
 end) in _
      ).
Removing explicit substitutions
Problems of sort