(6steps) PrintForm Definitions mb automata 3 Sections GenAutomata Doc

At: tproj w f 1
1. da: Collection(dec())
2. rho: Decl
3. tr: trace_env([[da]] rho)
4. y1: Label

tr.y1 {a:([[da]] rho)| tr.proj(y1,kind(a)) } List
By:
Unfold `tproj` 0
THEN
Unfold `trace_projection` 0
Generated subgoal:

1 filter(x.tr.proj(y1,kind(x));tr.trace) {a:([[da]] rho)| tr.proj(y1,kind(a)) } List

About:
listassertsetlambdaapplymember

(6steps) PrintForm Definitions mb automata 3 Sections GenAutomata Doc