proposition: Lemma substitution_closed_subterm : substitution_closed (@subterm Sig).
proof: Proof. intros t u s h. destruct h as [C h]. destruct h as [C0 h]. subst. rewrite sub_fill. exists (subc s C). split; try refl. destruct C. simpl. auto. discr. Qed.
imports: CoLoR(SN ASubstitution ATerm RelUtil AContext LogicUtil VecUtil NaryFunction) Coq(List)