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