fact: Definition evalB (s:state) (e:bExp) : option bool := match e with | bGt e1 e2 => match evalA s e1, evalA s e2 with | Some n1, Some n2 => match Z_le_gt_dec n1 n2 with | left _ => Some false | right _ => Some true end | _, _ => None (A:=bool) end end.
imports: ZArith Zwf Inverse_Image Wellfounded Extraction List Arith Compare_dec Lia