The Coq mailing list

[Gert Smolka <smolka AT ps.uni-saarland.de>]

I would like to prove

Inductive K (x: nat) : nat -> Type :=
| K1: K x (S x)
| K2: forall y z, K x y -> K y z -> K x z.

Fact K2_injective x y z a b a' b':
K2 x y z a b = K2 x y z a' b' -> (a,b) = (a',b').

by hand in a way that is similar to the proof generated 
by the dependent elimination tactic of the Equations package.
Does someone have a hand proof bringing across the essential ideas?

Thanks in advance,
Gert

PS. I have a simple proof exploiting the "semantic” fact (K x y -> x < y),
but so far I failed in finding a "regular” proof using only routine 
techniques.