Bug with definition of last on Vectors

[GuiltyDolphin]

The following example:

data Vec (n : Nat) (a : Type) where
  Nil : Vec 0 a;
  Cons : a -> Vec n a -> Vec (n + 1) a

last : forall {a : Type, k : Nat} . Vec (k + 1) (a [0..1]) -> a
-- when k = 0
last (Cons [x] Nil) = x;
-- when k = k' + 1
last (Cons [_] xs)  = last xs

Doesn't type check, it results in the following error:

The following theorem associated with `last` is falsifiable:
	∀ n0.1 : ↑Nat,a1.1 : Type,t2.1 : Type,t3.1 : ↑Nat . ((0..0 ≤ 0..1) ∧ (n0.1 + 1 = k + 1) -> (0..1 ≤ 0..1))

Ouch.

[dorchard]

For this we need to be able to propagate information between equations which we used to do, but realised we were doing it in not a fine-grained enough way. This would make a very useful project...