proposition: Lemma IR_substitution_closed : substitution_closed IR.
proof: Proof. unfold transp, substitution_closed, IR. intros t1 t2 s H xint0. rewrite !substitution_lemma. apply (H (beta xint0 s)). Qed.
imports: CoLoR(ATerm RelUtil ASubstitution NaryFunction AContext VecUtil SN ARelation LogicUtil) Coq(Lia PeanoNat)