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

At: tproj w f2 1 1 1 1 2
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
7. subtype_rel(({a:([[da]] rho)| tr.proj(y1,kind(a)) } List); (rho(lbl_pr( < Trace, y1 > ))))

({a:([[da]] rho)| tr.proj(y1,kind(a)) } List) (rho(lbl_pr( < Trace, y1 > )))
By: Unfold `subtype` 0
Generated subgoal:

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

About:
listassertsetapplymembersubtypeimpliesall

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