1 files changed, 5 insertions, 0 deletions
diff --git a/AAC.v b/AAC.v
index f6f382f..5feb0b6 100644
--- a/AAC.v
+++ b/AAC.v
@@ -1115,6 +1115,11 @@ Section s.
 End s.
 End Internal.
 
+Local Ltac internal_normalize :=
+  let x := fresh in let y := fresh in
+  intro x; intro y; vm_compute in x; vm_compute in y; unfold x; unfold y;
+  compute [Internal.eval Internal.fold_map Internal.copy Prect]; simpl.
+
 
 (** * Lemmas for performing transitivity steps
    given an instance of AAC_lift *)