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