proposition: Theorem statementAt_def_inv : forall b pc1 s, In s (statements b) -> STATEMENT.pc s = pc1 -> statementAt b pc1 = Some s.
proof: Proof. intros b0 pc1 s H1 H2. unfold statementAt. destruct (statementAtS b0 pc1) as [Ex|Ex]. case Ex. intros x P Q. assert (x=s). apply (PC_unique_impl x s b0). assumption. assumption. rewrite <- Q. auto. rewrite H; reflexivity. assert (pc1 <> pc s). apply (AllS_x_P STATEMENT.t (neq_PC_Stmt pc1) (statements b0) s Ex H1). unfold not in H. elim H. auto. 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)