fact: Definition interface (p:t) (en:TypeDefName) : option TYPEDEF.t := let eq_en (e:TYPEDEF.t) := eq_TypeDefName (TYPEDEF.name e) en in List.find eq_en (interfaces p).
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)