Get entire HTLgenspec proof passing

1 files changed, 10 insertions, 0 deletions

diff --git a/src/common/Vericertlib.v b/src/common/Vericertlib.v
index ef4a10b..33ddb71 100644
--- a/src/common/Vericertlib.v
+++ b/src/common/Vericertlib.v
@@ -84,6 +84,16 @@ Ltac solve_by_invert := solve_by_inverts 1.
 
 Ltac invert x := inversion x; subst; clear x.
 
+(** For a hypothesis of a forall-type, instantiate every variable to a fresh existential *)
+Ltac insterU H :=
+  repeat match type of H with
+         | forall x : ?T, _ =>
+           let x := fresh "x" in
+           evar (x : T);
+           let x' := eval unfold x in x in
+               clear x; specialize (H x')
+         end.
+
 Ltac destruct_match :=
   match goal with
   | [ |- context[match ?x with | _ => _ end ] ] => destruct x eqn:?