1 files changed, 28 insertions, 0 deletions
diff --git a/src/Core/Declarative/Substitution.idr b/src/Core/Declarative/Substitution.idr
new file mode 100644
index 0000000..bd37432
--- /dev/null
+++ b/src/Core/Declarative/Substitution.idr
@@ -0,0 +1,28 @@
+module Core.Declarative.Substitution
+
+import Core.Context
+import Core.Declarative
+import Core.Environment
+import Core.Thinning
+import Core.Term
+import Core.Term.Substitution
+
+-- Definition ------------------------------------------------------------------
+
+public export
+data SubstWf : Env sy -> Subst sx sy -> Env sx -> Type where
+  Base : IsExtension thin env2 env1 -> SubstWf env2 (Base thin) env1
+  (:<) :
+    SubstWf env2 sub env1 ->
+    TermWf env2 (expand t) (expand a) ->
+    SubstWf env2 (sub :< t) (Add env1 a)
+
+namespace Conv
+  public export
+  data SubstConv : Env sy -> Subst sx sy -> Subst sx sy -> Env sx -> Type where
+    Base : IsExtension thin env2 env1 -> SubstConv env2 (Base thin) (Base thin) env1
+    (:<) :
+      forall sub1, sub2.
+      SubstConv env2 sub1 sub2 env1 ->
+      TermConv env2 (expand t) (expand u) (expand a) ->
+      SubstConv env2 (sub1 :< t) (sub2 :< u) (Add env1 a)