(|proptest|
 (|thm| "" (FLATTEN)
  (("" (SPLIT)
    (("1" (PROPAX) NIL NIL)
     ("2" (SPLIT) (("1" (PROPAX) NIL NIL) ("2" (PROPAX) NIL NIL)) NIL)
     ("3" (PROPAX) NIL NIL))
    NIL))
  NIL)
 (|thm_2| "" (PROP) NIL NIL))