blob: 9d056c4ae0626a6f13c7db767678c68ee3ba2ffd (
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 = ?Goal : [q : nat n : nat m : nat |- n = ?y]
|
