(8steps) PrintForm Definitions Lemmas mb automata 3 Sections GenAutomata Doc

At: tproj w f2 1 1
1. da: Collection(dec())
2. rho: Decl
3. tr: trace_env([[da]] rho)
4. y1: Label
5. trace_consistent(rho;da;tr.proj;trace(y1))
6. tr.y1 {a:([[da]] rho)| tr.proj(y1,kind(a)) } List

tr.y1 rho(lbl_pr( < Trace, y1 > ))
By: ParallelOp -1
Generated subgoal:

1 ({a:([[da]] rho)| tr.proj(y1,kind(a)) } List) (rho(lbl_pr( < Trace, y1 > )))

About:
listassertsetapplymembersubtype

(8steps) PrintForm Definitions Lemmas mb automata 3 Sections GenAutomata Doc