proposition: Theorem last_elem : forall t pc, last t = Some pc -> elem t pc = true.
proof: Proof. intros b0 pc1 H. unfold last in H. destruct (lastS (statements b0)). destruct s. inversion H. apply (elem_def_inv b0 x). apply Last_In. assumption. discriminate H. 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)