Natural_deduction : ITM_main.subst_free_vars_in_fml_with

let rec subst_free_vars_in_fml_with_terms (subst : t_var -> t_term) (fml : t_fml) : t_fml =
        match fml with
        |PredApp (p, terms) ->
                let map (term : t_term) : t_term =
                        match term with
                        |Atom var -> subst var
                        |_ -> term
                in PredApp (p, List.map map terms)
        |UnopApp (unop, fml1) ->
                UnopApp (unop, subst_free_vars_in_fml_with_terms subst fml1)
        |BinopApp (binop, fml1, fml2) ->
                BinopApp (binop, subst_free_vars_in_fml_with_terms subst fml1, subst_free_vars_in_fml_with_terms subst fml2)
        |QuantApp (quant, var1, fml1) ->
                let new_subst (var : t_var) : t_term =
                        if var = var1 then Atom var else 
                        match List.mem var1 (FML_main.vars_of_terms [subst var]) with
                        |true -> raise (Cannot_replace_var_with_term_containing_var_in_fml (var, subst var, var1, fml))
                        |false -> subst var 
                in
                QuantApp (quant, var1, subst_free_vars_in_fml_with_terms new_subst fml1)