[Agda] Panic: CanSplit

[Wouter Swierstra]

Suppose I have the following definition of "less than or equal" for  
finite sets:

> data Nat : Set where
>   Zero : Nat
>   Succ  : (k : Nat) -> Nat
>
> data Fin : Nat -> Set where
>   fz : {n : Nat} -> Fin (Succ n)
>   fs : {n : Nat} -> Fin n -> Fin (Succ n)
>
> inj : {n : Nat} -> Fin n -> Fin (Succ n)
> inj fz = fz
> inj (fs i) = fs (inj i)
>
> data _<=_ : {n : Nat} -> Fin n -> Fin n -> Set where
>   Base : forall {n : Nat} {i : Fin n} -> i <= i
>   Step : forall {n : Nat} (i j : Fin n) -> i <= j -> inj i <= fs j

I would expect the following lemma to hold:

> fsLt : forall {n : Nat} (i j : Fin n) -> fs i <= fs j -> i <= j

Yet I'm struggling to prove it. The obvious proof, by doing a case  
split on "fs i <= fs j", gives me the rather cryptic error message:

   Panic: CantSplit Tmp.Step

I think this means that Agda cannot figure out how to invert the "inj"  
function that is produced by the Step constructor.

How can I work around this problem? Thanks in advance for any advice,

   Wouter