def substitute(t, subs):
    """
    Return the term obtained from t by simultaneous substitution given
    by subs

    subs is either a dictionary or a mapping given by an iterable of
    (key, value) pairs

    Both keys and values in subs can be either Var or Const.
    All keys in subs will be substituted by their values in subs.

    For variables, only free occurances will be substituted.

    If the substitution will create capturing of a free variable, the
    substitution will fail with an error.
    """

    if not isinstance(subs, dict):
        subs = dict(subs)

    if type(t) in (Var, Const):
        if t in subs:
            return subs[t]
        else:
            return t

    elif type(t) in (Apply, Eq, Ite, Not, And, Or, Implies, Iff):
        return type(t)(*(substitute(x, subs) for x in t))

    elif type(t) in (ForAll, Exists):
        forbidden_variables = free_variables(*subs.values())
        if forbidden_variables.isdisjoint(t.variables):
            return type(t)(t.variables, substitute(t.body, (
                (k, v) for k, v in subs.iteritems()
                if k not in t.variables
            )))
        else:
            assert False, (t, subs) # capturing would be created

    else:
        assert False, type(e)
dataset/ETHPy150Open Microsoft/ivy/ivy/logic_util.py/substitute/original