cj
Drule.cj : int -> thm -> thm
Returns the i'th conjunct of a "guarded" theorem
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.