fact: Fixpoint af (r:env)(a:aexpr) {struct a}: option Z := match a with avar index => lookup r index | anum n => Some n | aplus e1 e2 => bind (af r e1) (fun v1 => bind (af r e2) (fun v2 => Some (v1+v2))) end.
imports: ZArith List syntax Lia