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

At: st app functionality

a1,a2,b1,b2:Collection(SimpleType). a1 = a2 b1 = b2 st_app(a1;b1) = st_app(a2;b2)
By:
UnivCD
THEN
Unfold `col_equal` 0
THEN
RWW "member_st_app" 0
Generated subgoal:

11. a1: Collection(SimpleType)
2. a2: Collection(SimpleType)
3. b1: Collection(SimpleType)
4. b2: Collection(SimpleType)
5. a1 = a2
6. b1 = b2
x:SimpleType. (a:SimpleType. a b1 & ax a1) (a:SimpleType. a b2 & ax a2)

About:
impliesandallexists

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