let rec prf_of_prf_raw (prf_raw : t_prf_raw) : t_prf = match prf_raw with | Atomic_prf_raw fml_raw -> Atomic_prf (fml_of_fml_raw fml_raw) | Nullary_prf_raw (nullary_rule, fml_raw) -> Nullary_prf (nullary_rule, fml_of_fml_raw fml_raw) | Unary_prf_raw (prf_raw1, unary_rule, fml_raw) -> Unary_prf (prf_of_prf_raw prf_raw1, unary_rule, fml_of_fml_raw fml_raw) | Binary_prf_raw (prf_raw1, prf_raw2, binary_rule, fml_raw) -> Binary_prf (prf_of_prf_raw prf_raw1, prf_of_prf_raw prf_raw2, binary_rule, fml_of_fml_raw fml_raw) | Trinary_prf_raw (prf_raw1, prf_raw2, prf_raw3, trinary_rule, fml_raw) -> Trinary_prf (prf_of_prf_raw prf_raw1, prf_of_prf_raw prf_raw2, prf_of_prf_raw prf_raw3, trinary_rule, fml_of_fml_raw fml_raw)