diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2023-06-09 20:57:08 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2023-06-09 20:57:08 +0100 |
| commit | 08dc4443af7a43f2966ddfdb614a449368cf3a8d (patch) | |
| tree | 521a43f76545d89cd218e7094188440122171c51 | |
| parent | de6de7fe0978fa0be6bd6b48e872dc57f2e751c8 (diff) | |
| download | vericert-08dc4443af7a43f2966ddfdb614a449368cf3a8d.tar.gz vericert-08dc4443af7a43f2966ddfdb614a449368cf3a8d.zip | |
Prove abstract_sequence_evaluable
| -rw-r--r-- | src/hls/GiblePargenproof.v | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/hls/GiblePargenproof.v b/src/hls/GiblePargenproof.v index f0e5874..099d127 100644 --- a/src/hls/GiblePargenproof.v +++ b/src/hls/GiblePargenproof.v @@ -667,6 +667,8 @@ have been evaluable. eapply abstract_sequence_evaluable_fold; eauto; auto. - apply sem_empty. - reflexivity. + - apply all_preds_in_empty. + - inversion 1. - cbn; unfold evaluable_pred_list; inversion 1. Qed. |