proposition: Lemma rangeFreeVarsApp : forall sa sb, rangeFreeVars (sa++sb) = rangeFreeVars sa ++ rangeFreeVars sb.
proof: Proof. intros. unfold rangeFreeVars. rewrite <- flat_map_app. unfold ALRange. rewrite <- map_app. refl. Qed.
imports: Term AssociationList