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