pub fn sort_domains(premises: &[ProofExpr]) -> HashMap<String, Vec<ProofTerm>>Expand description
Per-sort domains: for each UNARY predicate used as a sort guard (Trip,
Year, …), the constants asserted to have it. Built from the ground facts the
declarations produce (Trip(Alpha), Trip(Beta), …). This is what lets
grounding expand ∀x(Trip(x)→…) over the 4 trips, not the whole universe.