WhoCites Definitions mb automata 4 Sections GenAutomata Doc

Who Cites tfvar?
tfvarDef l == tree_leaf(ts_fvar(l))
Thm* l:Label. l Term
ts_fvar Def ts_fvar(x) == inr(inr(inr(inl(x))))
Thm* x:Label. ts_fvar(x) ts()
tree_leaf Def tree_leaf(x) == inl(x)
Thm* E,T:Type, x:E. tree_leaf(x) tree_con(E;T)
Thm* E:Type, x:E. tree_leaf(x) Tree(E)

Syntax:l has structure: tfvar(l)

About:
inlinruniversememberall!abstraction

WhoCites Definitions mb automata 4 Sections GenAutomata Doc