proposition: Theorem statementAt_def : forall b pc1 s, statementAt b pc1 = Some s -> STATEMENT.pc s = pc1.
proof: Proof. intros b0 pc1 s H. unfold statementAt in H. destruct (statementAtS b0 pc1) as [Ex|]. case_eq Ex. intros x P Q ex. rewrite ex in H. inversion H. rewrite Q. rewrite H1. reflexivity. discriminate H. Qed.
imports: JML(JMLProgramPlus) Coq(ZArith) JML(ZHelpers) JML(LogicHelpers) Coq(Bool) Coq(Sumbool) Coq(Ndec) JML(PosAux) JML(EqBoolAux) Coq(Relation_Operators) Coq(List) JML(ListFunctions) JML(ListHelpers) JML(OptionHelpers)