(implies
    (and
      (commonModalityFeatures ?MODALOPSETFN iModExistFactoringOutFromDisj)
      (skolem ?MODALOPSETFN
        (tSetOfModalOpSetFn ?M-PRED ?SET-COL)))
    (theoremConditional
      (elementOf ?IND ?SET-COL)
      (implies
        (and
          (quotedIsa ?PROP2 CycLSentence-Assertible)
          (?M-PRED ?IND
            (exists ?X-1 ?SUB-PROP-1))
          (evaluate ?SUB-PROP-1
            (uSubstituteFormulaFn ?X ?A ?PROP1))
          (evaluate ?SUB-PROP-2
            (uSubstituteFormulaFn ?Y ?A
              (or ?PROP1 ?PROP2))))
        (?M-PRED ?IND
          (exists ?Y-1 ?SUB-PROP-2)))))