Natural_deduction : FML_main.subst_in

let rec subst_in_fml (var : t_var) (term : t_term) (fml : t_fml) : t_fml =
        match fml with
        | PredApp (pred, term_list) -> PredApp (pred, List.map (subst_in_term var term) term_list)
        | BinopApp (binop, fml1, fml2) -> BinopApp (binop, subst_in_fml var term fml1, subst_in_fml var term fml2)
        | UnopApp (unop, fml1) -> UnopApp (unop, subst_in_fml var term fml1)
        | QuantApp (quant, var1, fml1) -> 
                match var = var1 with
                |true -> QuantApp (quant, var1, fml1)
                |false -> QuantApp (quant, var1, subst_in_fml var term fml1)