r:rel(), te:(LabelLabel), rho,ds,da,de,e,s,a:Top. [[r]] rho ds da de e s a mk_trace_env(nil, te) ~ [[r]] rho ds da de e s a niltrace()

Analyze 0
THEN
Analyze 1
THEN
Unfold `rel_mng` 0
THEN
Reduce 0
THEN
Assert (te:(LabelLabel), rho,ds,da,de,e,s,a,x:Top. list_accum(x,t.x ([[t]] 1of(e) s a mk_trace_env(nil, te));x;r1) ~ list_accum(x,t....;x;r1))

1	1. name: relname() 2. r1: Term List te:(LabelLabel), rho,ds,da,de,e,s,a,x:Top. list_accum(x,t.x ([[t]] 1of(e) s a mk_trace_env(nil, te));x;r1) ~ list_accum(x,t.x([[t]] 1of(e) s a niltrace());x;r1)
2	1. name: relname() 2. r1: Term List 3. te:(LabelLabel), rho,ds,da,de,e,s,a,x:Top. list_accum(x,t.x ([[t]] 1of(e) s a mk_trace_env(nil, te));x;r1) ~ list_accum(x,t.x([[t]] 1of(e) s a niltrace());x;r1) te:(LabelLabel), rho,ds,da,de,e,s,a:Top. list_accum(x,t.x ([[t]] 1of(e) s a mk_trace_env(nil, te));[[name]] rho 2of(e) ;r1) ~ list_accum(x,t....;...;r1)

About: