theorem Lean.Grind.intro_with_eq (p : Prop) (p' : Prop) (q : Prop) (he : p = p') (h : p' → q) : p → q