def substitute(formula, variable, constant, logic):
    """Substitutes the free ocurrences of variable in formula for constant"""

    # Atomic
    if len(formula) == 1:
        return [formula[0].replace(variable, constant)]

    # Unary connective:
    if len(formula) == 2 and formula[0] in logic.constants(1):
        return [formula[0], substitute(formula[1], variable, constant, logic)]

    # Binary connective:
    if len(formula) == 3 and formula[1] in logic.constants(2):
        return [substitute(formula[0], variable, constant, logic), formula[1],
                substitute(formula[2], variable, constant, logic)]

    # Quantifier
    if len(formula) == 3 and formula[0] in logic.quantifiers:
        # If the variable is the same that is being replaced, do nothing
        if formula[1] == variable:
            return formula
        else:
            return [formula[0], formula[1], substitute(formula[2], variable, constant, logic)]