-- (ir1, .., irn) = f qtvs givens
-- where f is (evidence for) the new implication constraint
-- f :: forall qtvs. givens => (ir1, .., irn)
-- (ir1, .., irn) = f qtvs givens
-- where f is (evidence for) the new implication constraint
-- f :: forall qtvs. givens => (ir1, .., irn)