proposition: Lemma Last_head_singleton : forall b s x, Suffix s (statements b) -> head s = Some x -> Last x s -> s = x::nil.
proof: Proof. intros. destruct s. discriminate H0. destruct s. inversion H0; reflexivity. inversion H0. assert (neq_PC_Stmt (pc x) x). apply AllS_x_P with (l := t1::s). apply Stmts_unique with (b := b0). rewrite <- H3; assumption. apply Last_In. apply Last_step_inv with (y := t0). intro Hdis; discriminate Hdis. assumption. auto. unfold neq_PC_Stmt in H2. elim H2; reflexivity. 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)