public static Proposition invertForallAroundGoal(Proposition forallprop, Proposition goal, Keyword headortail, boolean contrapositiveP) {
    { KeyValueMap mapping = KeyValueMap.newKeyValueMap();
      Proposition invertedforall = Proposition.copyProposition(forallprop, mapping);
      Stella_Object oldhead = (invertedforall.arguments.theArray)[1];
      Stella_Object oldtail = (invertedforall.arguments.theArray)[0];
      Proposition newgoal = ((Proposition)(mapping.lookup(goal)));
      Cons newgoalarguments = Proposition.extractGoalArguments(newgoal);
      Proposition headprime = null;
      Proposition tailprime = null;
      Proposition newhead = null;
      Proposition newtail = null;

      if (contrapositiveP) {
        oldhead = Proposition.invertProposition(((Proposition)(oldhead)));
        oldtail = Proposition.invertProposition(((Proposition)(oldtail)));
        newgoal = Proposition.extractInvertedGoal(((headortail == Logic.KWD_HEAD) ? ((Proposition)(oldhead)) : ((Proposition)(oldtail))), newgoal);
        if (newgoal == null) {
          {
            System.out.println("Unable to generate contrapositive rule for goal `" + goal + "'");
            System.out.println("in `" + forallprop + "'");
          }
;
          return (null);
        }
        (invertedforall.arguments.theArray)[0] = oldhead;
        (invertedforall.arguments.theArray)[1] = oldtail;
        oldhead = oldtail;
        oldtail = (invertedforall.arguments.theArray)[0];
        headortail = ((headortail == Logic.KWD_HEAD) ? Logic.KWD_TAIL : Logic.KWD_HEAD);
      }
      { boolean testValue000 = false;

        testValue000 = newgoal == (((headortail == Logic.KWD_HEAD) ? oldhead : oldtail));
        if (testValue000) {
          { boolean alwaysP000 = true;

            { Stella_Object arg = null;
              Cons iter000 = newgoalarguments;
              PatternVariable v = null;
              Vector vector000 = ((Vector)(KeyValueList.dynamicSlotValue(invertedforall.dynamicSlots, Logic.SYM_LOGIC_IO_VARIABLES, null)));
              int index000 = 0;
              int length000 = vector000.length();

              loop000 : for (;(!(iter000 == Stella.NIL)) &&
                        (index000 < length000); iter000 = iter000.rest, index000 = index000 + 1) {
                arg = iter000.value;
                v = ((PatternVariable)((vector000.theArray)[index000]));
                if (!(arg == v)) {
                  alwaysP000 = false;
                  break loop000;
                }
              }
            }
            testValue000 = alwaysP000;
          }
          if (testValue000) {
            testValue000 = newgoalarguments.length() == ((Vector)(KeyValueList.dynamicSlotValue(invertedforall.dynamicSlots, Logic.SYM_LOGIC_IO_VARIABLES, null))).length();
          }
        }
        if (testValue000) {
          return (invertedforall);
        }
      }
      if (headortail == Logic.KWD_HEAD) {
        headprime = Proposition.substituteProposition(((Proposition)(oldhead)), newgoal, Logic.FALSE_PROPOSITION);
        Proposition.normalizeProposition(headprime);
        if (headprime.operator == Logic.SGT_STELLA_FALSE) {
          newtail = ((Proposition)(oldtail));
        }
        else {
          {
            oldtail = Proposition.invertProposition(((Proposition)(oldtail)));
            newtail = Logic.disjoinPropositions(Cons.consList(Cons.cons(oldtail, Cons.cons(headprime, Stella.NIL))));
            newtail = Proposition.invertProposition(newtail);
            Proposition.normalizeProposition(newtail);
          }
        }
        (invertedforall.arguments.theArray)[0] = newtail;
        (invertedforall.arguments.theArray)[1] = newgoal;
      }
      else if (headortail == Logic.KWD_TAIL) {
        tailprime = Proposition.substituteProposition(((Proposition)(oldtail)), newgoal, Logic.TRUE_PROPOSITION);
        Proposition.normalizeProposition(tailprime);
        if (tailprime.operator == Logic.SGT_STELLA_TRUE) {
          newhead = ((Proposition)(oldhead));
        }
        else {
          { Cons residuevariables = Stella.NIL;

            tailprime = Proposition.invertProposition(tailprime);
            newhead = Logic.disjoinPropositions(Cons.consList(Cons.cons(tailprime, Cons.cons(oldhead, Stella.NIL))));
            { PatternVariable vbl = null;
              Vector vector001 = ((Vector)(KeyValueList.dynamicSlotValue(invertedforall.dynamicSlots, Logic.SYM_LOGIC_IO_VARIABLES, null)));
              int index001 = 0;
              int length001 = vector001.length();
              Cons collect000 = null;

              for (;index001 < length001; index001 = index001 + 1) {
                vbl = ((PatternVariable)((vector001.theArray)[index001]));
                if (!newgoalarguments.memberP(vbl)) {
                  if (collect000 == null) {
                    {
                      collect000 = Cons.cons(vbl, Stella.NIL);
                      if (residuevariables == Stella.NIL) {
                        residuevariables = collect000;
                      }
                      else {
                        Cons.addConsToEndOfConsList(residuevariables, collect000);
                      }
                    }
                  }
                  else {
                    {
                      collect000.rest = Cons.cons(vbl, Stella.NIL);
                      collect000 = collect000.rest;
                    }
                  }
                }
              }
            }
            if (!(residuevariables == Stella.NIL)) {
              { Proposition nestedforall = Logic.createProposition(Logic.SYM_STELLA_FORALL, 2);

                KeyValueList.setDynamicSlotValue(nestedforall.dynamicSlots, Logic.SYM_LOGIC_IO_VARIABLES, Logic.copyConsListToVariablesVector(residuevariables), null);
                (nestedforall.arguments.theArray)[0] = Logic.TRUE_PROPOSITION;
                (nestedforall.arguments.theArray)[1] = newhead;
                newhead = nestedforall;
              }
            }
            Proposition.normalizeProposition(newhead);
          }
        }
        (invertedforall.arguments.theArray)[0] = newgoal;
        (invertedforall.arguments.theArray)[1] = newhead;
      }
      else {
        { OutputStringStream stream000 = OutputStringStream.newOutputStringStream();

          stream000.nativeStream.print("`" + headortail + "' is not a valid case option");
          throw ((StellaException)(StellaException.newStellaException(stream000.theStringReader()).fillInStackTrace()));
        }
      }
      { Cons newvariables = Proposition.extractGoalArguments(newgoal);

        { Stella_Object v = null;
          Cons iter001 = newvariables;
          int i = Stella.NULL_INTEGER;
          int iter002 = 0;

          for (;!(iter001 == Stella.NIL); iter001 = iter001.rest, iter002 = iter002 + 1) {
            v = iter001.value;
            i = iter002;
            if (!Stella_Object.isaP(v, Logic.SGT_LOGIC_PATTERN_VARIABLE)) {
              { PatternVariable constantvbl = Logic.createVariable(null, null, false);

                Skolem.updateSkolemType(constantvbl, Logic.logicalType(v));
                newvariables.nthSetter(constantvbl, i);
                if (headortail == Logic.KWD_HEAD) {
                  (invertedforall.arguments.theArray)[0] = (Proposition.conjoinTwoPropositions(Logic.createEquivalenceProposition(constantvbl, v), ((Proposition)((invertedforall.arguments.theArray)[0]))));
                }
                else if (headortail == Logic.KWD_TAIL) {
                  { Proposition negatedequivalence = Logic.createEquivalenceProposition(constantvbl, v);

                    Proposition.invertProposition(negatedequivalence);
                    (invertedforall.arguments.theArray)[1] = (Logic.disjoinPropositions(Cons.consList(Cons.cons(negatedequivalence, Cons.cons((invertedforall.arguments.theArray)[1], Stella.NIL)))));
                  }
                }
                else {
                  { OutputStringStream stream001 = OutputStringStream.newOutputStringStream();

                    stream001.nativeStream.print("`" + headortail + "' is not a valid case option");
                    throw ((StellaException)(StellaException.newStellaException(stream001.theStringReader()).fillInStackTrace()));
                  }
                }
                Proposition.normalizeProposition(((Proposition)((invertedforall.arguments.theArray)[0])));
              }
            }
          }
        }
        KeyValueList.setDynamicSlotValue(invertedforall.dynamicSlots, Logic.SYM_LOGIC_IO_VARIABLES, Logic.copyConsListToVariablesVector(newvariables), null);
      }
      Proposition.recursivelyFastenDownPropositions(invertedforall, false);
      return (invertedforall);
    }
  }