proposition: Lemma AvRenamingSubset : forall {G : CFGV} {vc : VarSym G} (lvl lvr : list (vType vc)) (sw : Swapping vc), subset lvr lvl -> AvRenaming lvl sw -> AvRenaming lvr sw.
proof: Proof. unfold AvRenaming. introv Hs Hav. repnd. dands; cpx. SetReasoning. Qed.
imports: AlphaEqProps Omega