| A.False -> mk_ident "False"
| A.Eq (l,r)
| A.NotEq (l,r) -> (* removes the negation *)
| A.False -> mk_ident "False"
| A.Eq (l,r)
| A.NotEq (l,r) -> (* removes the negation *)
in
build_ctx_for_arities universally
(List.map (fun x -> (x,0)) (collect_fv_from_atom a)) (aux a)
in
build_ctx_for_arities universally
(List.map (fun x -> (x,0)) (collect_fv_from_atom a)) (aux a)
convert_formula fv false context f)
in
let o = PT.Theorem (`Theorem,name,f,None) in
convert_formula fv false context f)
in
let o = PT.Theorem (`Theorem,name,f,None) in