From ce546fe96974cb7aa3b09c729f33ac6ba5169299 Mon Sep 17 00:00:00 2001
From: Greg Brown <greg.brown01@ed.ac.uk>
Date: Mon, 10 Jul 2023 13:37:56 +0100
Subject: Describe unification.

---
 src/Data/Fin/Occurs.idr | 11 +++++++++++
 1 file changed, 11 insertions(+)

(limited to 'src/Data/Fin/Occurs.idr')

diff --git a/src/Data/Fin/Occurs.idr b/src/Data/Fin/Occurs.idr
index 58c8faa..d70c8f3 100644
--- a/src/Data/Fin/Occurs.idr
+++ b/src/Data/Fin/Occurs.idr
@@ -101,3 +101,14 @@ thickJust (FS x) (FS y) prf =
   let 0 z = mapJustInverse suc (thick x y) prf in
   rewrite snd $ z.snd in
   trans (thinSucSuc x z.fst) (cong FS $ thickJust x y (fst $ z.snd))
+
+export
+thickThin : (x : Fin n) -> (y : Fin (pred n)) -> thick x (thin x y) = Just y
+thickThin x y =
+  let neq = thinSkips x y in
+  let isJust = thickNeq x (thin x y) (\prf => neq $ sym prf) in
+  let zPrf = extractIsJust isJust in
+  let z = zPrf.fst in
+  let 0 prf1 = zPrf.snd in
+  let 0 prf2 = thickJust x (thin x y) prf1 in
+  trans prf1 (cong Just $ thinInjective x prf2)
-- 
cgit v1.2.3