module Obs.Substitution

import Data.Fin

public export
interface Rename (x : Nat -> Type) where
  rename : forall m, n . x n -> (Fin n -> Fin m) -> x m

public export
interface Subst (x, y, z : Nat -> Type) where
  subst : forall m, n . x n -> (Fin n -> y m) -> z m