proposition: Lemma context_closed_comp : forall R S, context_closed R -> context_closed S -> context_closed (R @ S).
proof: Proof. intros R S hR hS t v c [u [h1 h2]]. exists (fill c u). split. apply hR. hyp. apply hS. hyp. Qed.
imports: CoLoR(SN ASubstitution ATerm RelUtil AContext LogicUtil VecUtil NaryFunction) Coq(List)