Describe unification.

1 files changed, 11 insertions, 0 deletions

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)