proposition: Lemma eq_primitiveType_spec : forall x y, if eq_primitiveType x y then x = y else x <> y.
proof: Proof. destruct x;destruct y;simpl;trivial; intro;discriminate. 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)