fact: Fixpoint lookup (idx:nat) (s:state) {struct idx} : option Z := match idx, s with | O, a :: _ => Some a | S p, _ :: tl => lookup p tl | _, _ => None (A:=Z) end.
imports: ZArith Zwf Inverse_Image Wellfounded Extraction List Arith Compare_dec Lia