diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/coq/Sail_values.v | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/lib/coq/Sail_values.v b/lib/coq/Sail_values.v index 0dc25e1b..2343490b 100644 --- a/lib/coq/Sail_values.v +++ b/lib/coq/Sail_values.v @@ -19,6 +19,9 @@ Lemma use_ArithFact {P} `(ArithFact P) : P. apply fact. Defined. +Definition build_ex (n:Z) {P:Z -> Prop} `{H:ArithFact (P n)} : {x : Z & ArithFact (P x)} := + existT _ n H. + Definition ii := Z. Definition nn := nat. |