fact: Definition eq_t (x y : t) : bool := let (n1,p1,r1) := x in let (n2,p2,r2) := y in (Z_eqb n1 n2) && (list_eq _ PARAM.eq_t p1 p2) && (opt_eq _ eq_type r1 r2).
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)