Definitions
bool
1
Doc
At:
eq
int
cases
test
A:Type, x,y:A, P:(A
Prop), i,j:
. P(if i=
j
x else y fi)
P(if i=
j
x else y fi)
By:
UnivCD
Generated subgoal:
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)