bool(1)

PINST tyin tmin th instantiates types in th according to tyin and terms
according to tmin.

 # let th = MESON[] `(x:A = y) <=> (y = x)`;;
 ...
 val th : thm = |- x = y <=> y = x

 # PINST [`:num`,`:A`] [`2 + 2`,`x:A`; `4`,`y:A`] th;;
 val it : thm = |- 2 + 2 = 4 <=> 4 = 2 + 2

PROVE_HYP th1 th2
If the conclusion of th1 is a hypothesis of th2, then returns th2
except that this hypothesis is replaced by the hypotheses of th1; otherwise
returns th2 unchanged.
いわゆる．カットです．

# let th1 = CONJUNCT2 (ASSUME `p /\ q /\ r`)
  and th2 = CONJUNCT2 (ASSUME `q /\ r`)
  and th3 = ADD_ASSUM `s:bool` th2;;
val th1 : thm = p /\ q /\ r |- q /\ r
val th2 : thm = q /\ r |- r
val th3 : thm = s, q /\ r |- r
# PROVE_HYP th1 th2;;
val it : thm = p /\ q /\ r |- r
# PROVE_HYP th1 th3;;
val it : thm = s, p /\ q /\ r |- r