At:
assert eq relname
4
1.
y1: Label
2.
y: Label
3.
inr(y1) = inr(y) 
SimpleType+Label
y1 =
y
By:
ApFunToHypEquands `z' Case(z) Case a = > a Default = > y Label -1
THEN
Reduce -1
THEN
Analyze -1
THEN
Reduce 0
Generated subgoal:
| 1 | 4. y1 = y
y1 = y |
About:
