proposition: Theorem next_elem : forall t pc1 pc2, next t pc1 = Some pc2 -> elem t pc2 = true.
proof: Proof. intros block pc1 pc2. unfold next. destruct (suffixS (statements block) pc1). destruct s; destruct s. case_eq (tail x). intros _ Hdis; discriminate Hdis. intros n tl Htl Hpc. inversion Hpc. apply elem_def_inv. apply Suffix_In with (s := x). intuition. destruct x. discriminate Htl. simpl in Htl. rewrite Htl. intuition auto with datatypes. intro Hdis; discriminate Hdis. 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)