rho:Decl, r:rel(), da:Collection(dec())
, R:(Label
Label
). 
rel_mentions_trace(r) 
trace_consistent_rel(rho;da;R;r)r:rel().
rel_mentions_trace(r) 
(
i:
. i < ||r.args|| & mentions_trace(r.args[i]))| Theorem | Name |
|
Thm* rho:Decl, r:rel(), da:Collection(dec())
, R:(LabelLabel). rel_mentions_trace(r) trace_consistent_rel(rho;da;R;r) | [no_mention_implies_consistent_rel] |
| cites | |
|
Thm* r:rel().
rel_mentions_trace(r) (i:. i < ||r.args|| & mentions_trace(r.args[i])) | [rel_mentions_trace_iff] |