From 67ba392ddddef079f7ed2e04b266b1b0029f1bf5 Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Sat, 10 Jun 2023 14:12:45 +0100
Subject: Try to prove main theorem

Missing some link between forests
---
 src/hls/GiblePargenproof.v | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/src/hls/GiblePargenproof.v b/src/hls/GiblePargenproof.v
index 90c132c..d9436b5 100644
--- a/src/hls/GiblePargenproof.v
+++ b/src/hls/GiblePargenproof.v
@@ -853,6 +853,11 @@ have been evaluable.
 (*    { inv H. inv H8. exists pr'. intros x0. specialize (H x0). auto. } *)
     simplify.
     exploit abstr_seq_reverse_correct; eauto.
+    { inv H8. inv H14.
+      eapply check_evaluability1_evaluable.
+      eauto. eauto.
+      eapply abstract_sequence_evaluable.
+      }
     admit. admit. reflexivity. simplify.
     exploit seqbb_step_parbb_step; eauto; intros.
     econstructor; split; eauto.
-- 
cgit