Natural_deduction : FML_main.closed_terms_of

let rec closed_terms_of_fml (fml : t_fml) : t_term list =
        match fml with
        | PredApp (_, term_list) -> closed_terms_of_term_list term_list
        | BinopApp (_, fml1, fml2) -> List.concat [closed_terms_of_fml fml1;closed_terms_of_fml fml2]
        | UnopApp (_, fml1) -> closed_terms_of_fml fml1
        | QuantApp (_, _, fml1) -> closed_terms_of_fml fml1

and closed_terms_of_term_list (term_list : t_term list) : t_term list =
        List.flatten (List.map closed_terms_of_term term_list)

and closed_terms_of_term (term : t_term) : t_term list =
        match term with
        |Atom _ -> []
        |FuncApp (_,[]) -> [term]
        |FuncApp (_, term_list) ->
                match is_closed_term term with
                |true -> term::(closed_terms_of_term_list term_list)
                |false -> closed_terms_of_term_list term_list