HepLean Documentation
Init
.
Grind
.
Lemmas
Search
Google site search
return to top
source
Imports
Init.Core
Imported by
Lean
.
Grind
.
intro_with_eq
source
theorem
Lean
.
Grind
.
intro_with_eq
(p p' q :
Prop
)
(he :
p
=
p'
)
(h :
p'
→
q
)
:
p
→
q