Function exactly 

pub fn exactly(vars: &[ProofExpr], k: usize, aux: &str) -> ProofExpr

“Exactly k of vars are true.”