proposition: Lemma IR_inclusion : R << R' -> IR R << IR R'.
proof: Proof. intro. unfold inclusion, IR. intros. apply H. apply H0. Qed.
imports: CoLoR(ATerm RelUtil ASubstitution NaryFunction AContext VecUtil SN ARelation LogicUtil) Coq(Lia PeanoNat)