blob: 52e1e0ed0107d3170cf567326acc0f5f8d5b2764 (
plain)
1
2
3
4
5
|
Existential 1 =
?Goal1 : [p : nat q := S p : nat n : nat m : nat |- ?y = m]
Existential 2 =
?y : [p : nat q := S p : nat n : nat m : nat |- nat] (p, q cannot be used)
Existential 3 = ?Goal0 : [q : nat n : nat m : nat |- n = ?y]
|
