Subst

Require Import internalize_tac Equality Nat.

Internalized Substitution

Instance term_subst : internalized subst.
Proof.
  internalizeR.
  revert ; induction y; intros k;recStep P; crush.
  destruct nat_eq_dec;dec;try tauto;crush.
Defined.