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

At: tproj w f2 1 1 1 1 1
1. da: Collection(dec())
2. rho: Decl
3. tr: trace_env([[da]] rho)
4. y1: Label
5. g:Label. y1 = g subtype_rel(({a:([[da]] rho)| tr.proj(g,kind(a)) } List); (rho(lbl_pr( < Trace, g > ))))
6. tr.y1 {a:([[da]] rho)| tr.proj(y1,kind(a)) } List

y1 = y1
By: EqLblReflexive 0
Generated subgoals:

None

About:
listassertsetapplymemberimpliesall

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