(9steps) PrintForm Definitions Lemmas mb automata 1 Sections GenAutomata Doc

At: assert st eq 1
1. s1: SimpleType
2. s2: SimpleType
3. st_eq(s1;s2)

s1 = s2
By:
MoveToConcl 2
THEN
MoveToConcl 1
Generated subgoal:

1 s1,s2:SimpleType. st_eq(s1;s2) s1 = s2

About:
assertequalimpliesall

(9steps) PrintForm Definitions Lemmas mb automata 1 Sections GenAutomata Doc