proposition: Lemma rc_substitution_closed : substitution_closed R -> substitution_closed E.
proof: Proof. intro. unfold substitution_closed, clos_refl, union. intros. decomp H0. subst t2. auto. right. apply H. hyp. Qed.
imports: CoLoR(SN ASubstitution ATerm RelUtil AContext LogicUtil VecUtil NaryFunction) Coq(List)