Natural_deduction : FML_main.fml_is_fml_with_var_replaced_by

let fml_is_fml_with_var_replaced_by_term (inst : t_fml) (fml : t_fml) (var : t_var) : t_term option =
        let rec aux (term_list : t_term list) : t_term option =
                match term_list with
                |[] -> None
                |hd::tl -> 
                        match inst = subst_in_fml var hd fml with
                        |true -> Some hd
                        |false -> aux tl
        in
        aux (closed_terms_of_fml inst)