fact: Fixpoint un_annot (i:a_instr):instr := match i with prec _ i => un_annot i | a_skip => skip | a_assign x e => assign x e | a_sequence i1 i2 => sequence (un_annot i1)(un_annot i2) | a_while b a i => while b (un_annot i) end.
imports: ZArith List String Bool syntax little axiom abstract_i