Ltac clear_duplicates_step := match goal with | [ H : ?T, H' : ?T |- _ ] => clear H' | [ H := ?T, H' := ?T |- _ ] => clear H' end. Ltac clear_duplicates := repeat clear_duplicates_step.