proposition: Lemma PI_term_int_eq : forall (xint : valuation I) t k (H : (maxvar t <= k)%nat), proj1_sig (term_int xint t) = proj1_sig (peval_D (bterm_poly_pos (inject_term H)) (vec_of_val xint (S k))).
proof: Proof. intros xint t k H. rewrite <- (term_int_eq_bterm_int xint H). gen (PI_bterm_int_eq xint (inject_term H)). intuition. Qed.
imports: CoLoR(ATerm ABterm ListUtil VecUtil PositivePolynom AInterpretation ZUtil NaryFunction ARelation RelUtil LogicUtil SN Polynom MonotonePolynom NatUtil ATrs BoundNat AWFMInterpretation ZUtil ACompat AMannaNess)