How to prove equality impossible

Question

1 subgoal
a, b : Tipe
H : TApp a b = a
______________________________________(1/1)
False

(where TApp is a constructor)

In Idris this can be proved with \Refl => impossible but I haven't managed to write any proof for it in Coq.

Is there an easy way to prove it?

Answer 1

You can prove it by induction a.. The idea is that the induction principle for Tipe encodes the fact that its values are finite in size, while the TApp a b = a assumption allows you to construct an infinite value, but these are somewhat indirect consequences from the raw facts you have, hence you need to work a bit for it. An extension of Coq to derive and use such occurs-check lemmas automatically would definitely be possible.