Proving dependent equalities in Coq with SSReflect

Proving dependent equalities in Coq is boring, but quite frequently done. I got so annoyed with it that I wrote a little tactic to automatize it a bit.

It does use ssreflect routines but it should not be hard to adapt it to vanilla Coq.

Ltac depcomp H := apply EqdepFacts.eq_sigT_eq_dep in H; 
apply Coq.Logic.Eqdep.EqdepTheory.eq_dep_eq in H.
Ltac eq_comp c x y := 
  move: (c x y); 
  case; 
  last try do [by [right; case]| 
  right; case; let H' := fresh "H" in move=>H'; by depcomp H'];
  first try let H' := fresh "H" in move=> H'; subst.


Definition eq_dec T := forall x y: T, {x = y} + {~ x = y}.

(* Example *)
Theorem pair_eq_dec T U: eq_dec T -> eq_dec U -> eq_dec (prod T U).
move=> HT HU [x y] [a b].
eq_comp HT x a.
eq_comp HU y b.
by left.
Qed.