proposition: Theorem elem_def : forall t pc, elem t pc = true -> exists s, statementAt t pc = Some s /\ STATEMENT.pc s = pc.
proof: Proof. intros b0 pc1 in_b0. unfold elem in in_b0. case_eq (statementAtS b0 pc1). intros sS H. destruct sS. exists x. split. unfold statementAt. rewrite H. reflexivity. auto. intros. rewrite H in in_b0. discriminate in_b0. 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)