proposition: Lemma compound_is_compound : forall body:t, exists bl, STATEMENT.type (compound body) = Compound bl /\ STATEMENT.label (compound body) = Some L_beginBody.
proof: Proof. intro body. exists (block body). simpl. split; 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)