proposition: Lemma IR_reflexive : reflexive R -> reflexive IR.
proof: Proof. intro. unfold reflexive, IR. auto. Qed.
imports: CoLoR(ATerm RelUtil ASubstitution NaryFunction AContext VecUtil SN ARelation LogicUtil) Coq(Lia PeanoNat)