WhoCites Definitions mb automata 4 Sections GenAutomata Doc

Who Cites trace env proj?
trace_env_projDef t.proj == 2of(t)
Thm* d:Decl, t:trace_env(d). t.proj LabelLabel
pi2 Def 2of(t) == t.2
Thm* A:Type, B:(AType), p:(a:AB(a)). 2of(p) B(1of(p))

Syntax:t.proj has structure: trace_env_proj(t)

About:
spreadproductboolfunctionuniversememberall!abstraction

WhoCites Definitions mb automata 4 Sections GenAutomata Doc