public static ControlFrame createConditionalAntecedentSubframe(ControlFrame frame, Proposition goal, Proposition provablerule) {
    { ControlFrame downframe = ControlFrame.createSubgoalFrame(frame, goal, Logic.KWD_CONDITIONAL_ANTECEDENT);
      ConditionalAntecedentProofAdjunct proofadjunct = ConditionalAntecedentProofAdjunct.newConditionalAntecedentProofAdjunct();

      KeyValueList.setDynamicSlotValue(downframe.dynamicSlots, Logic.SYM_LOGIC_PROOF_ADJUNCT, proofadjunct, null);
      proofadjunct.provableRule = provablerule;
      proofadjunct.goal = goal;
      return (downframe);
    }
  }