Home / Glossary / Lifting rule

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.