Natural_deduction : FML_main.vars_of

let rec vars_of_terms (term_list : t_term list) : t_var list =
        let rec aux (lst : t_term list) (acc : t_var list) : t_var list =
                match lst with
                |[] -> acc
                |hd::tl ->
                        match hd with
                        |Atom (var : t_var) -> aux tl (var::acc)
                        |FuncApp (_, terms) -> aux tl (List.concat [acc;vars_of_terms terms])
        in List.rev (aux term_list [])