proposition: Lemma AlphaEqSubstApp : forall (sla slb sra srb : SSubstitution vc), AlphaEqSubst sla sra -> AlphaEqSubst slb srb -> AlphaEqSubst (sla ++ slb) (sra ++ srb).
proof: Proof. intros. apply ALRangeRelApp. dands; trivial. Qed.
imports: Term AssociationList Swap AlphaEqProps SubstAux