Function ground 

pub fn ground(e: &ProofExpr, domain: &[ProofTerm]) -> ProofExpr

Ground every quantifier in e over domain (Herbrand expansion): a universal becomes the conjunction of its instances, an existential the disjunction. The returned expression is quantifier-free when domain covers the universe.

Sound AND complete for a domain-CLOSED finite problem (every individual named): ∀x.φ ≡ ⋀_c φ[x:=c] and ∃x.φ ≡ ⋁_c φ[x:=c] exactly when the witness/ counter-example is guaranteed to be one of the c.