let uguard_dnf sigma args tr_args = function | [] -> [] | [j, dnf] -> let uargs = List.filter (fun a -> not (H.list_mem a tr_args)) args in List.map (fun i -> List.map (fun sa -> SAtom.subst ((j, i)::sigma) sa) dnf) uargs | _ -> assert false