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