2. t: Term
3. da: Collection(dec())
4. R: Label
Label
5. g: Label
6. term_mentions_guard(g;t)
rho 
LabelType 
rho:Decl, t:Term, da:Collection(dec()), R:(LabelLabel). trace_consistent(rho;da;R;t) Prop| 1 | 1. rho: Decl 2. t: Term 3. da: Collection(dec()) 4. R: Label Label5. g: Label 6. term_mentions_guard(g;t) rho LabelType |
About:
 |  |  |  |  |  |