proposition: Lemma substitution_closed_subterm_eq : substitution_closed (@subterm_eq Sig).
proof: Proof. intros t u s h. destruct h as [C h]. subst. rewrite sub_fill. exists (subc s C). refl. Qed.
imports: CoLoR(SN ASubstitution ATerm RelUtil AContext LogicUtil VecUtil NaryFunction) Coq(List)