At:
tc pred addprime21
1.
P: Fmla
2.
ds: Collection(dec())
3.
da: Collection(SimpleType)
4.
de: sig()
5.
r:rel(). r (P)' tc(r;ds;da;de)
6.
r: rel()
7.
r P
(r)' (P)'
By:
Unfold `pred_addprime` 0
THEN
RW ColMemberC 0
THEN
InstConcl [r]
THEN
Try (Fold `pred` 0)
Generated subgoals:
r:rel(). r 
(P)' 
tc(r;ds;da;de)
(r)'