LIST_CONJ : thm list -> thm
A1 |- t1 ... An |- tn ---------------------------------- LIST_CONJ A1 u ... u An |- t1 /\ ... /\ tn