LET_ELIM_TAC splits conjuncts.

[ordinarymath]

Theorem let_elim_repro:
    let x = y z q
    in
    A x /\ B x
Proof
   LET_ELIM_TAC

In here LET_ELIM_TAC splits the goal into two subgoals

2 subgoals:
val it =
   
    0.  Abbrev (x = y z q)
   ------------------------------------
        B x
   
    0.  Abbrev (x = y z q)
   ------------------------------------
        A x