At: tc addprime r:rel(), ds:Collection(dec()), da:Collection(SimpleType), de:sig().
tc(r;ds;da;de) tc((r)';ds;da;de) By: Auto
THEN
All (Unfolds [`tc`;`rel_addprime`])
THEN
Analyze 1
THEN
Analyze 1
THEN
All Reduce
THEN
ExRepD
THEN
Analyze 0
THEN
Try (All (RWW "map_length_nat"))
THEN
All (RWW "map_select")
THEN
All Reduce
THEN
Try (RWW "map_length_nat" -1)
THEN
Try
(Complete
((Subst (term_types(ds;da;de;(r1[0])') ~ term_types(ds;da;de;r1[0])) 0) THEN (Try Trivial)
THEN
(Try
(BackThru
Thm*t:Term, ds,da,de:Top.
term_types(ds;da;de;(t)') ~ term_types(ds;da;de;t)))))
THEN
Try
(Complete
((Subst (term_types(ds;da;de;(r1[1])') ~ term_types(ds;da;de;r1[1])) 0) THEN (Try Trivial)
THEN
(Try
(BackThru
Thm*t:Term, ds,da,de:Top.
term_types(ds;da;de;(t)') ~ term_types(ds;da;de;t)))))
THEN
Try
(Complete
((Subst (term_types(ds;da;de;(r1[i])') ~ term_types(ds;da;de;r1[i])) 0) THEN (Try Trivial)
THEN
(Try
(BackThru
Thm*t:Term, ds,da,de:Top.
term_types(ds;da;de;(t)') ~ term_types(ds;da;de;t)))
THEN
(Try BackThruSomeHyp)))
THEN
Try
(Complete
((Subst (term_types(ds;da;de;(r1[0])') ~ term_types(ds;da;de;r1[0])) -3) THEN (Try Trivial)
THEN
(Try
(BackThru
Thm*t:Term, ds,da,de:Top.
term_types(ds;da;de;(t)') ~ term_types(ds;da;de;t)))))
THEN
Try
(Complete
((Subst (term_types(ds;da;de;(r1[1])') ~ term_types(ds;da;de;r1[1])) -2) THEN (Try Trivial)
THEN
(Try
(BackThru
Thm*t:Term, ds,da,de:Top.
term_types(ds;da;de;(t)') ~ term_types(ds;da;de;t)))))
THEN
Try
(Complete
((All (InstHyp [i]))
THEN
(Subst (term_types(ds;da;de;(r1[i])') ~ term_types(ds;da;de;r1[i])) -1)
THEN
(Try Trivial)
THEN
(Try
(BackThru
Thm*t:Term, ds,da,de:Top.
term_types(ds;da;de;(t)') ~ term_types(ds;da;de;t)))
THEN
(Try BackThruSomeHyp)))
THEN
Try (Complete Auto) Generated subgoals:
r:rel(), ds:Collection(dec()), da:Collection(SimpleType), de:sig().
tc(r;ds;da;de) 
tc((r)';ds;da;de)