fact: Definition swapAbs (a : Abstraction) (sw : Swapping vc) : Abstraction := match a with | termAbs _ lbv t => termAbs (swapLVar sw lbv) (tSwap t sw) | patAbs _ lbv t => patAbs (swapLVar sw lbv) (pSwap t sw) end.
imports: Swap