let premises_of_prf (excluded : t_fml list) (prf : t_prf): t_fml list = let rec aux (prf : t_prf): t_fml list = match prf with |Atomic_prf fml -> if List.mem fml excluded then [] else [fml] |Nullary_prf (_, fml) -> [] |Unary_prf (prf1,_,_) -> aux prf1 |Binary_prf (prf1, prf2, _, _) -> List.concat [aux prf1; aux prf2] |Trinary_prf (prf1, prf2, prf3, _, _) -> List.concat [aux prf1; aux prf2; aux prf3] in enumerate (aux prf)