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