proposition: Lemma pAlphaEqEquivariantRev : forall (sw : Swapping vc) s (ta tb : Pattern s), pAlphaEq vc (pSwap ta sw) (pSwap tb sw) -> pAlphaEq vc ta tb.
proof: Proof. introv Hd. apply (tcase alphaEquiVariant) in Hd. specialize (Hd (rev sw)). autorewrite with SwapAppR in Hd. autorewrite with fast in Hd. trivial. Qed.
imports: AlphaEquality SwapProps