public static Proposition deriveImpliesFromForall(Proposition forallprop) {
    { List heads = Proposition.findMatchableGoals(forallprop, Logic.KWD_HEAD);
      List tails = Proposition.findMatchableGoals(forallprop, Logic.KWD_TAIL);
      Proposition headgoal = ((Proposition)(heads.first()));
      Proposition tailgoal = ((Proposition)(tails.first()));
      Proposition headproposition = ((Proposition)((forallprop.arguments.theArray)[1]));
      Proposition tailproposition = ((Proposition)((forallprop.arguments.theArray)[0]));

      { boolean testValue000 = false;

        testValue000 = heads.length() == 1;
        if (testValue000) {
          testValue000 = tails.length() == 1;
          if (testValue000) {
            { boolean alwaysP000 = true;

              { Stella_Object hv = null;
                Vector vector000 = headgoal.arguments;
                int index000 = 0;
                int length000 = vector000.length();
                Stella_Object tv = null;
                Vector vector001 = tailgoal.arguments;
                int index001 = 0;
                int length001 = vector001.length();

                loop000 : for (;(index000 < length000) &&
                          (index001 < length001); index000 = index000 + 1, index001 = index001 + 1) {
                  hv = (vector000.theArray)[index000];
                  tv = (vector001.theArray)[index001];
                  if (!(Stella_Object.eqlP(hv, tv) &&
                      Stella_Object.isaP(hv, Logic.SGT_LOGIC_PATTERN_VARIABLE))) {
                    alwaysP000 = false;
                    break loop000;
                  }
                }
              }
              testValue000 = alwaysP000;
            }
            if (testValue000) {
              testValue000 = headgoal.arguments.length() == tailgoal.arguments.length();
              if (testValue000) {
                testValue000 = ((Proposition)(heads.first())) == headproposition;
                if (testValue000) {
                  if (((Proposition)(tails.first())) == tailproposition) {
                    testValue000 = true;
                  }
                  else {
                    {
                      testValue000 = tailproposition.kind == Logic.KWD_AND;
                      if (testValue000) {
                        { boolean alwaysP001 = true;

                          { Stella_Object arg = null;
                            Vector vector002 = tailproposition.arguments;
                            int index002 = 0;
                            int length002 = vector002.length();

                            loop001 : for (;index002 < length002; index002 = index002 + 1) {
                              arg = (vector002.theArray)[index002];
                              if (!(arg == tailgoal)) {
                                alwaysP001 = false;
                                break loop001;
                              }
                            }
                          }
                          testValue000 = alwaysP001;
                        }
                      }
                    }
                  }
                }
              }
            }
          }
        }
        if (testValue000) {
          return (Logic.createImpliesProposition(Proposition.extractGoalDescription(tailgoal, null), Proposition.extractGoalDescription(headgoal, null)));
        }
        else {
          return (null);
        }
      }
    }
  }