proposition: Lemma tSSubstAuxSubFilter: forall (suba subb: SSubstitution vc) (lv : list (vType vc)), disjoint lv (rangeFreeVars suba) -> tSSubstAux_sub suba (SubFilter subb lv) = tSSubstAux_sub suba subb.
proof: Proof. induction suba as [|(v,t) suba Hind]; introv Hdis ; cpx;[]. simpl. unfold rangeFreeVars in Hdis. simpl in Hdis. repeat(disjoint_reasoning). f_equal; cpx;[]. f_equal. symmetry. apply SSubstAuxSubFilter. disjoint_reasoning. Qed.
imports: Term AssociationList