At:
term mng2 addprime t:Term, e,s,s',a,tr:Top. [[(t)']] e s s' a tr ~ [[t]] e s' a tr
By:
Analyze 0
THEN
All (Unfolds [`term_mng`;`term_mng2`;`addprime`])
THEN
TermInd 1
THEN
Reduce 0
THEN
Try (Complete Auto)
THEN
All (Folds [`term_mng`;`term_mng2`;`addprime`])
THEN
Try (UnivCD THEN Analyze THEN BackThruSomeHyp)
Generated subgoals:
t:Term, e,s,s',a,tr:Top. [[(t)']] e s s' a tr ~ [[t]] e s' a tr