def DerivingHelpers.tacticDeriving_ReflEq_tactic : Lean.ParserDescr

theorem DerivingHelpers.and_true_curry {a b : Bool} {P : Prop} (h : a = true → b = true → P) : (a && b) = true → P

theorem DerivingHelpers.deriving_lawful_beq_helper_dep {α : Type u_1} {x y : α} [BEq α] [ReflBEq α] {t : (x == y) = true → Bool} {P : Prop} (inst : (x == y) = true → x = y) (k : ∀ (h : x = y), t ⋯ = true → P) : (if h : (x == y) = true then t h else false) = true → P

theorem DerivingHelpers.deriving_lawful_beq_helper_nd {α : Type u_1} {x y : α} [BEq α] [ReflBEq α] {P : Prop} (inst : (x == y) = true → x = y) (k : x = y → P) : (x == y) = true → P

def tacticDeriving_LawfulEq_tactic_step : Lean.ParserDescr

def tacticDeriving_LawfulEq_tactic : Lean.ParserDescr