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