fact: Fixpoint noAssign (n:nat) (i:inst nat aExp bExp) {struct i} : bool := match i with | Skip _ _ _ => true | Scolon i1 i2 => match noAssign n i1 with | true => noAssign n i2 | false => false end | WhileDo b i' => noAssign n i' | Assign v e => match eq_nat_dec v n with | left _ => false | right _ => true end end.
imports: ZArith Zwf Inverse_Image Wellfounded Extraction List Arith Compare_dec Lia