Definitions
bool
1
Doc
At:
eq
int
cases
test
1
1.
A:
Type
2.
x:
A
3.
y:
A
4.
P:
A
Prop
5.
i:
6.
j:
7.
P(if i=
j
x else y fi)
P(if i=
j
x else y fi)
By:
EqIntCases 7
Generated subgoals:
1
7.
P(x)
8.
i = j
P(if i=
j
x else y fi)
2
7.
P(y)
8.
i
j
P(if i=
j
x else y fi)