A lifting rule is a rule with an #$ist
(or #$liftTo
) in the arg 0 position of the consequent literal. The purpose is to overrule the Mt placement of the conclusion with placement into another Mt, maybe found via some combination of antecedent literals.