fact: Fixpoint eq_type (t1 t2: StaticType) {struct t1} : bool := match t1, t2 with | ReferenceType rt1, ReferenceType rt2 => eq_reftype rt1 rt2 | PrimitiveType pt1, PrimitiveType pt2 => eq_primitiveType pt1 pt2 | _, _ => false end with eq_reftype (rt1 rt2: refType) {struct rt1} : bool := match rt1, rt2 with | ArrayType t1 _, ArrayType t2 _ => eq_type t1 t2 | TypeDefType en1 _, TypeDefType en2 _ => eq_TypeDefName en1 en2 |_, _ => false end.
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)