Module Funind_plugin.Indfun

val functional_induction : bool -> EConstr.constr -> (EConstr.constr * EConstr.constr Tactypes.bindings) option -> Tactypes.or_and_intro_pattern option -> unit Proofview.tactic