# 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.