fact: Definition expressionSubstitute (x:Expression) (eq_x : Expression -> bool) (t:Expression) (e:Expression) : Expression := let mapF (y:Expression) : Expression := match eq_x y with | true => t | false => y end in expressionMap mapF e.
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)