Library Prelude.Tactics
Ltac ssubst :=
lazymatch goal with
| [ H : existT _ _ _ = existT _ _ _ |- _ ]
=> apply Eqdep.EqdepTheory.inj_pair2 in H;
ssubst
| [ |- _]
=> subst
end.
lazymatch goal with
| [ H : existT _ _ _ = existT _ _ _ |- _ ]
=> apply Eqdep.EqdepTheory.inj_pair2 in H;
ssubst
| [ |- _]
=> subst
end.