Do not handle ENCODE_EQ_INTRO in LFSC (cvc5#11439)

This rule was updated from a previous version ENCODE_PRED_TRANSFORM, but
the LFSC printer was never updated to handle this, we drop support for
this.

Fixes 2 of the failing regressions in the nightlies.

Also downgrades a warning to a trace message, fixing a further issue in
the nightlies.

src/proof/lfsc/lfsc_printer.cpp

@@ -540,11 +540,6 @@ void LfscPrinter::printProofInternal(
           Assert(passumeIt != passumeMap.end());
           out->printId(passumeIt->second, d_assumpPrefix);
         }
-        else if (r == ProofRule::ENCODE_EQ_INTRO)
-        {
-          // just add child
-          visit.push_back(PExpr(cur->getChildren()[0].get()));
-        }
         else if (isLambda)
         {
           Assert(cur->getArguments().size() == 3);

src/smt/proof_post_processor_dsl.cpp

@@ -96,8 +96,9 @@ void ProofPostprocessDsl::reconstruct(
     Trace("pp-dsl") << "REM SUBGOALS: " << std::endl;
     for (std::shared_ptr<ProofNode> p : d_subgoals)
     {
-      Warning() << "WARNING: unproven subgoal " << p->getResult() << std::endl;
       Trace("pp-dsl") << "  " << p->getResult() << std::endl;
+      Trace("pp-dsl-warn") << "WARNING: unproven subgoal " << p->getResult()
+                           << std::endl;
     }
     d_subgoals.clear();
   }