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