proposition: Lemma PC_unique_impl : forall x y b, In x (statements b) -> In y (statements b) -> pc x = pc y -> x = y.
proof: Proof. intros. assert ((exists s, Suffix (x::s) (statements b0) /\ In y (x::s)) \/ (exists s, Suffix (y::s) (statements b0) /\ In x (y::s))). apply Suffix_x_y_or_y_x; assumption. case H2; clear H2. intro H3. elim H3; intros. destruct H2. elim H4. intuition. intro H5. assert (neq_PC_Stmt (pc x) y). apply AllS_x_P with (l := x0). apply Stmts_unique with (b := b0); assumption. assumption. unfold neq_PC_Stmt in H6. elim H6; auto. intro H3. elim H3; intros. destruct H2. elim H4. intuition. intro H5. assert (neq_PC_Stmt (pc y) x). apply AllS_x_P with (l := x0). apply Stmts_unique with (b := b0); assumption. assumption. unfold neq_PC_Stmt in H6. elim H6; 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)