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

At: member st app1 1
1. s1: Tree(Label+Unit)
2. s2: SimpleType
3. s: SimpleType
4. u: Tree(Label+Unit)Type{i'}
5. w: s1:{v:Tree(Label+Unit)| u(v) }s st_app1(s1;s2) st_eq(s1;s2s)
6. x: Label+Unit

s < > st_eq(tree_leaf(x);tree_node( < s2, s > ))
By: (RWW "member_col_none" 0) THENA (Auto THEN (Unfold `st` 0) THEN (Fold `st` 0))
Generated subgoal:

1 False st_eq(tree_leaf(x);tree_node( < s2, s > ))

About:
assertunitunionsetapplyfunctionuniversefalse

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