proposition: Lemma tRenWithSpec : forall {G : CFGV} {vc : VarSym G} (s : GSym G) (ta : Term s) (lvA : list (vType vc)), {tar : Term s $ tAlphaEq vc ta tar # disjoint (tBndngVarsDeep vc tar) lvA}.
proof: Proof. intros. exists (tRenAlpha ta lvA). pose proof (@RenAlphaAlpha G vc). pose proof (@RenAlphaAvoid G vc). repnd. dands; cpx. Qed.
imports: AlphaEqProps Omega