let rec transform_prf (f : t_fml -> t_fml) (prf : t_prf) : t_prf = match prf with |Atomic_prf fml -> Atomic_prf (f fml) |Nullary_prf (rule, fml) -> Nullary_prf (rule, f fml) |Unary_prf (prf1, rule, fml) -> Unary_prf (transform_prf f prf1, rule, f fml) |Binary_prf (prf1, prf2, rule, fml) -> Binary_prf (transform_prf f prf1, transform_prf f prf2, rule, f fml) |Trinary_prf (prf1, prf2, prf3, rule, fml) -> Trinary_prf (transform_prf f prf1, transform_prf f prf2, transform_prf f prf3, rule, f fml)