proposition: Lemma IR'_incl_IR : IR' << IR.
proof: Proof. unfold inclusion, IR, IR'. intros. set (m := max (maxvar x) (maxvar y)). assert (maxvar x <= m). unfold m. apply Nat.le_max_l. assert (maxvar y <= m). unfold m. apply Nat.le_max_r. assert (term_int xint x = term_int (fval xint (1+m)) x). apply term_int_eq_fval_lt. lia. rewrite H2. assert (term_int xint y = term_int (fval xint (1+m)) y). apply term_int_eq_fval_lt. lia. rewrite H3. unfold fval. apply H. Qed.
imports: CoLoR(ATerm RelUtil ASubstitution NaryFunction AContext VecUtil SN ARelation LogicUtil) Coq(Lia PeanoNat)