proposition: Lemma IR_WF : WF R -> WF IR.
proof: Proof. intro. set (xint := fun x:nat => some_elt I). apply (WF_incl (fun t1 t2 => R (term_int xint t1) (term_int xint t2))). unfold Basics.flip, inclusion. auto. apply (WF_inverse (term_int xint) H). Qed.
imports: CoLoR(ATerm RelUtil ASubstitution NaryFunction AContext VecUtil SN ARelation LogicUtil) Coq(Lia PeanoNat)