proposition: Theorem elem_def_inv : forall t s0, In s0 (statements t) -> elem t (STATEMENT.pc s0) = true.
proof: Proof. intros. unfold elem. destruct (statementAtS t0 (pc s0)). destruct s as (s1,_,_). reflexivity. assert (neq_PC_Stmt (pc s0) s0). apply AllS_x_P with (l := statements t0); assumption. unfold neq_PC_Stmt in H0. 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)