Restart.

- use De Bruijn, as Namely, Painless had more pain than promised;
- remove higher-kinded types;
- provide ill-typing predicates;
- prove substitution respects ill-typing;

1 files changed, 0 insertions, 6 deletions

diff --git a/src/Inky/Erased.idr b/src/Inky/Erased.idr
deleted file mode 100644
index 05bb29e..0000000
--- a/src/Inky/Erased.idr
+++ /dev/null
@@ -1,6 +0,0 @@
-module Inky.Erased
-
-public export
-record Erased (t : Type) where
-  constructor Forget
-  0 val : t