proposition: Lemma swapSubSwitch : forall (sub: SSubstitution vc)(sw : Swapping vc), swapSub sub sw = swapSub sub (ALSwitch sw).
proof: Proof. induction sub; cpx. intros. simpl. f_equal; cpx. f_equal. - apply swapVarSwitch. - apply swapSwitch. Qed.
imports: Term AssociationList Swap AlphaEqProps SubstAux