`impossible` keyword works but there is a valid case

[worudso]

Steps to Reproduce

data Even: Nat -> Type where
  EvenZ: Even Z
  EvenS: Even n -> Even (n + 2)

total
lemma1: Even Z
lemma1 = EvenZ

total
lemma2: Even Z
lemma2 x impossible -- Idris says 'lemma2 x is a valid case' and I agree with you

total
lemma3: Even 2
lemma3 = EvenS EvenZ

total
lemma4: Even 2 -> Void
lemma4 x impossible -- what does it work?

total
lemma5: Even 1 -> Void
lemma5 x impossible

Expected Behavior

lemma4 can't be proved.

Observed Behavior

lemma4 has been passed type check

I posted a question about impossible on StackOverflow not knowing this behavior can be a bug. Here is the link. https://stackoverflow.com/questions/60190106/idris-impossible-keyword-proves-a-wrong-proposition And I got an answer that says Idris didn't work as expected with my example. My Idris version is 1.3.2