proposition: Lemma AlphaEqAbsPSameParam : forall (gsa gsb : GSym G) (lbva lbvb: list vcType) (tma : Pattern gsa) (tmb : Pattern gsb), AlphaEqAbs (patAbs vc lbva tma) (patAbs vc lbvb tmb) -> gsa =gsb.
proof: Proof. introv Hal. inversion Hal. auto. Qed.
imports: AlphaEquality SwapProps Eqdep_dec