proposition: Lemma alSSubstAux_MakeAbstractionsTNode : forall p ma sub, alSSubstAux (MakeAbstractionsTNode vc p ma) sub = MakeAbstractions vc (mSSubstAux ma (lBoundVars vc (bndngPatIndices p) ma) sub) (lBoundVars vc (bndngPatIndices p) (mSSubstAux ma (lBoundVars vc (bndngPatIndices p) ma) sub)).
proof: Proof. unfold MakeAbstractionsTNode, MakeAbstractionsTNodeAux. intros p ma sub. rw <- lBoundVarsSameSSubstAux. remember (lBoundVars vc (bndngPatIndices p) ma). clear Heql. revert l sub. induction ma; introv; allsimpl; auto; destruct l; allsimpl; auto; unfold SubFilter; try (rw ALFilter_nil_r); apply eq_cons; auto. Qed.
imports: Term AssociationList Swap AlphaEqProps SubstAux