At: term mng nil u:Term, te:(LabelLabel), e,s,a:Top. [[u]] e s a mk_trace_env(nil, te) ~ [[u]] e s a niltrace() By: Analyze 0
THEN
TermInd 1
THEN
Reduce 0
THEN
UnivCD
THEN
Try (Complete Auto)
THEN
Try ((Unfolds [`niltrace`;`tproj`] 0) THEN (Reduce 0) THEN (Complete Auto))
THEN
Try (Analyze THEN BackThruSomeHyp THEN (Complete Auto)) Generated subgoals:
u:Term, te:(Label
Label
), e,s,a:Top. [[u]] e s a mk_trace_env(nil, te) ~ [[u]] e s a niltrace()