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

At: assert eq relname 4 1
1. y1: Label
2. y: Label
3. inr(y1) = inr(y) SimpleType+Label
4. y1 = y

y1 = y
By:
HypSubst -1 0
THEN
EqLblReflexive 0
Generated subgoals:

None

About:
assertunioninrequal

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