fact: Fixpoint interp_PElist (l:list R) (lpe:list (PExpr C * PExpr C)) {struct lpe} : Prop := match lpe with | nil => True | (me,pe)::lpe => match lpe with | nil => PEeval l me == PEeval l pe | _ => PEeval l me == PEeval l pe /\ interp_PElist l lpe end end.
imports: Setoid BinList BinPos BinNat BinInt Ring_polynom Ncring