At:
tc pred unprime1
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 pred_unprime(P)
tc(r;ds;da;de)
By:
Unfold `pred_unprime` -1
THEN
RW ColMemberC -1
THEN
ExRepD
THEN
SubstFor r 0
THEN
RWO "tc_unprime < " 0
THEN
BackThruSomeHyp
Generated subgoals:
r:rel(). r 
P 
tc(r;ds;da;de)
tc(r;ds;da;de)