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