cj : int -> thm -> thm
STRUCTURE
SYNOPSIS
Returns the i’th conjunct of a “guarded” theorem
DESCRIPTION
A call to cj i th, where th has the form
   |- !x1 .. xn. p1 /\ .. /\ pm ==> !y... q1 /\ .. ==> ... ==>
                                          c1 /\ c2 /\ ... ck
returns the theorem
   |- !x1 .. xn. p1 /\ .. /\ pm ==> !y... q1 /\ .. ==> ... ==> ci
Note that the indexing starts at 1. The conjuncts are stripped apart without regard to the way in which they are associated, as per the behaviour of CONJUNCTS.
FAILURE
Fails if the conclusion of the guarded theorem does not contain at least i conjuncts. A bare term is always considered to be 1 conjunct.
SEEALSO
HOL  Trindemossen-1