pub fn lift_quantifier<'a>( kind: QuantifierKind, restrictor: Symbol, interner: &mut Interner, expr_arena: &'a Arena<LogicExpr<'a>>, term_arena: &'a Arena<Term<'a>>, ) -> &'a LogicExpr<'a>