def var_in(t, x):
    if is_var(t):
        return t == x
    elif x in t:
        return True
    elif True in [var_in(i, x) for i in t]:
        return True
    else:
        return False

    
def ext(t, level=0, max=10):
    if is_var(t):
        return t
    
    var = level + hash("extensionality var")
    y = simp([t, var])
    
    #this is stupid
    if not level > max:
        y = ext(y, level+1)
        
    if y == var:
        return "I"
    if not is_node(y):
        return t
    elif var == y[1] and (not var_in(y[0], var)):
        return y[0]
    elif not var_in(y, var):
        return ext(["K", ext(y)], level+1)
    else:
        return t