proposition: Lemma substitution_closed_transp : forall R, substitution_closed R -> substitution_closed (transp R).
proof: Proof. intros R hR t u s. unfold transp. apply hR. Qed.
imports: CoLoR(SN ASubstitution ATerm RelUtil AContext LogicUtil VecUtil NaryFunction) Coq(List)