fact: Fixpoint AGeval (vm : list G) (e : AGExpr) : G := match e with | AGX j => nth zeroG vm j | AGO => zeroG | AGOpp e1 => oppG (AGeval vm e1) | AGAdd e1 e2 => addG (AGeval vm e1) (AGeval vm e2) end.
imports: Coq(ZArith)