At: term types unprime t:Term, ds,da,de:Top. term_types(ds;da;de;unprime(t)) ~ term_types(ds;da;de;t) By: Analyze 0
THEN
Unfolds [`term_types`;`unprime`] 0
THEN
TermInd 1
THEN
Reduce 0
THEN
All (Folds [`term_types`;`unprime`])
THEN
Try (Complete Auto)
THEN
Try (UnivCD THEN Analyze THEN BackThruSomeHyp) Generated subgoals:
t:Term, ds,da,de:Top. term_types(ds;da;de;unprime(t)) ~ term_types(ds;da;de;t)