proposition: Lemma tSSubstAux_sub_trivial: forall (suba subb : SSubstitution vc) (Hdis: disjoint (rangeFreeVars suba) (ALDom subb)), tSSubstAux_sub suba subb = suba.
proof: Proof. induction suba; intros; cpx;[]. unfold rangeFreeVars in Hdis. simpl in Hdis. disjoint_reasoning. allsimpl. simpl. f_equal; auto;[]. f_equal. apply SSubstAuxTrivial. trivial. Qed.
imports: Term AssociationList