sig val at : Clause_intf.S.t -> Logtk.Position.t -> Logtk.FOTerm.t end