proposition: Lemma substitution_closed_rtc : forall R, substitution_closed R -> substitution_closed (R #).
proof: Proof. intros R h t u s. induction 1. apply rt_step. apply h. hyp. apply rt_refl. apply rt_trans with (sub s y); hyp. Qed.
imports: CoLoR(SN ASubstitution ATerm RelUtil AContext LogicUtil VecUtil NaryFunction) Coq(List)