Definition Subst := R (.\"Subst", "s", "k", "u"; "s" (.\"n"; !EqN "n" "k" "u" (!Var "n"))
                                                     (.\"s1", "s2"; !App ("Subst" "s1" "k" "u") ("Subst" "s2" "k" "u"))
                                                     (.\"s1"; !Lam ("Subst" "s1" (!Succ "k") "u")) ).

Lemma Subst_correct s k u :
  Subst (tenc s) (enc k) (tenc u) == tenc (subst s k u).