public static Proposition inheritProposition(Proposition self, KeyValueMap mapping) {
    { Keyword testValue000 = self.kind;

      if ((testValue000 == Logic.KWD_FORALL) ||
          (testValue000 == Logic.KWD_EXISTS)) {
        { Object old$Evaluationmode$000 = Logic.$EVALUATIONMODE$.get();

          try {
            Native.setSpecial(Logic.$EVALUATIONMODE$, Logic.KWD_DESCRIPTION);
            return (Proposition.copyProposition(self, mapping));

          } finally {
            Logic.$EVALUATIONMODE$.set(old$Evaluationmode$000);
          }
        }
      }
      else if (testValue000 == Logic.KWD_FUNCTION) {
        { Stella_Object value = Logic.inheritPropositionArgument((self.arguments.theArray)[(self.arguments.length() - 1)], self, mapping);
          Proposition copy = null;

          if (value == null) {
            return (null);
          }
          copy = Proposition.findSimilarProposition(self, mapping);
          if (copy == null) {
            copy = Proposition.inheritFunctionProposition(self, mapping, true);
            copy = Proposition.eradicateHoldsProposition(copy);
          }
          if (Stella_Object.eqlP((copy.arguments.theArray)[(copy.arguments.length() - 1)], value)) {
            copy = Logic.TRUE_PROPOSITION;
          }
          else {
            copy = Skolem.inheritEquivalentProposition(((Skolem)((copy.arguments.theArray)[(copy.arguments.length() - 1)])), value);
          }
          mapping.insertAt(self, copy);
          return (copy);
        }
      }
      else {
      }
    }
    { Proposition matchingproposition = ((Proposition)(mapping.lookup(self)));

      if (matchingproposition != null) {
        return (matchingproposition);
      }
      if (BooleanWrapper.coerceWrappedBooleanToBoolean(self.variableTypeP())) {
        { Stella_Object binding = mapping.lookup((self.arguments.theArray)[0]);

          if ((binding != null) &&
              (!Logic.skolemP(binding))) {
            return (Logic.TRUE_PROPOSITION);
          }
        }
      }
      if (matchingproposition != null) {
        mapping.insertAt(self, matchingproposition);
        return (matchingproposition);
      }
    }
    { GeneralizedSymbol operator = self.operator;
      List argumentsmapto = List.newList();
      Proposition copy = null;
      Stella_Object argmapsto = null;

      { Stella_Object arg = null;
        Vector vector000 = self.arguments;
        int index000 = 0;
        int length000 = vector000.length();
        Cons collect000 = null;

        for (;index000 < length000; index000 = index000 + 1) {
          arg = (vector000.theArray)[index000];
          argmapsto = Logic.inheritPropositionArgument(arg, self, mapping);
          if (argmapsto == null) {
            return (null);
          }
          if (collect000 == null) {
            {
              collect000 = Cons.cons(argmapsto, Stella.NIL);
              if (argumentsmapto.theConsList == Stella.NIL) {
                argumentsmapto.theConsList = collect000;
              }
              else {
                Cons.addConsToEndOfConsList(argumentsmapto.theConsList, collect000);
              }
            }
          }
          else {
            {
              collect000.rest = Cons.cons(argmapsto, Stella.NIL);
              collect000 = collect000.rest;
            }
          }
        }
      }
      copy = Logic.createProposition(Logic.SYM_LOGIC_CONSTANT, 0);
      copy.kind = self.kind;
      copy.operator = operator;
      copy.arguments = Logic.copyListToArgumentsVector(argumentsmapto);
      if (BooleanWrapper.coerceWrappedBooleanToBoolean(self.variableTypeP())) {
        KeyValueList.setDynamicSlotValue(copy.dynamicSlots, Logic.SYM_LOGIC_VARIABLE_TYPEp, Stella.TRUE_WRAPPER, null);
      }
      copy = Proposition.eradicateHoldsProposition(copy);
      mapping.insertAt(self, copy);
      return (copy);
    }
  }