+ Tactic Definition TGenBase :=
+ Match Context With
+ | [ H: (TSort ?) = (TSort ?) |- ? ] -> Inversion H; Clear H
+ | [ H: (TLRef ?) = (TLRef ?) |- ? ] -> Inversion H; Clear H
+ | [ H: (TTail ? ? ?) = (TTail ? ? ?) |- ? ] -> Inversion H; Clear H
+ | _ -> Idtac.
+