From 60df32ffd5b88498e4634649509bbd0810421004 Mon Sep 17 00:00:00 2001
From: Greg Brown <greg.brown01@ed.ac.uk>
Date: Tue, 11 Jul 2023 16:25:24 +0100
Subject: Begin big unification proof.

---
 src/Data/Term/Zipper.idr | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'src/Data/Term/Zipper.idr')

diff --git a/src/Data/Term/Zipper.idr b/src/Data/Term/Zipper.idr
index 608e86c..ddc0797 100644
--- a/src/Data/Term/Zipper.idr
+++ b/src/Data/Term/Zipper.idr
@@ -115,6 +115,10 @@ actionHomo f (Op op i ts zip) t = cong (Op op) $ Calc $
   ~~ insertAt' i (f <$> zip + t) (map (f <$>) ts)           ...(mapInsertAt (f <$>) i (zip + t) ts)
   ~~ insertAt' i ((f <$> zip) + (f <$> t)) (map (f <$>) ts) ...(cong (\t => insertAt' i t (map (f <$>) ts)) $ actionHomo f zip t)
 
+export
+invertActionTop : (zip : Zipper sig k) -> (0 _ : f <$> zip = Top) -> zip = Top
+invertActionTop Top prf = Refl
+
 -- Cycles ----------------------------------------------------------------------
 
 pivotAt : sig.Operator k -> SFin k -> Vect k (Term sig n) -> Zipper sig n
-- 
cgit v1.2.3