CONJUNCT1 : thm -> thm
STRUCTURE
SYNOPSIS
Extracts left conjunct of theorem.
DESCRIPTION
    A |- t1 /\ t2
   ---------------  CONJUNCT1
       A |- t1

FAILURE
Fails unless the input theorem is a conjunction.
COMMENTS
The theorem AND1_THM can be instantiated to similar effect.
SEEALSO
HOL  Kananaskis-13