fun substitute variables expr =
let
    fun kleisliMap _ tl [] = ([], tl)
    | kleisliMap f tl (hd::tail) = let
        val (res, tl2) = f tl hd
        val (xs, tl3) = kleisliMap f tl2 tail
    in
        (res::xs, tl3)
    end
    fun substitute (hd::tail) expr =
        (case expr of
            True => (True, hd::tail)
            | False => (False, hd::tail)
            | Variable var => if contains (hd::tail) var then raise InvalidVariable
                              else (Variable var, hd::tail)
            | Equiv (left, right) =>
                let
                    val (l, remaining) = substitute tail left
                    val (r, remaining) = substitute remaining right
                in
                    (Equiv (Variable hd, Equiv (l, r)), remaining)
                end
            | Implies (left, right) =>
                let
                    val (l, remaining) = substitute tail left
                    val (r, remaining) = substitute remaining right
                in
                    (Equiv (Variable hd, Implies (l, r)), remaining)
                end
            | And expressions =>
                let
                    val (expressions, tail) = kleisliMap substitute tail expressions
                in
                    (Equiv (Variable hd, And expressions), tail)
                end
            | Or expressions =>
                let
                    val (expressions, tail) = kleisliMap substitute tail expressions
                in
                    (Equiv (Variable hd, Or expressions), tail)
                end
            | Not expr =>
                let
                    val (e, remaining) = substitute tail expr
                in
                    (Equiv (Variable hd, Not e), remaining)
                end)
        | substitute [] expr =
            case expr of
                Or _ => raise InsufficientVariables
                | And _ => raise InsufficientVariables
                | Implies _ => raise InsufficientVariables
                | Equiv _ => raise InsufficientVariables
                | Not _ => raise InsufficientVariables
                | e => (e, [])
    val (res, _) = substitute variables expr
in
    res
end;