fact: Definition freevars_abs (a : Abstraction G vc) := match a with | termAbs _ vars t => subtractv (tfreevars vc t) vars | patAbs _ vars p => subtractv (pfreevars vc p) vars end.
imports: AlphaEquality SwapProps Eqdep_dec