Cc_plugin.Cctac
val congruence_tac : int -> EConstr.constr list -> unit Proofview.tactic
val simple_congruence_tac : int -> EConstr.constr list -> unit Proofview.tactic
val f_equal : unit Proofview.tactic