theorem
proved
term proof
voice_forcing_chain
show as:
view Lean formalization →
formal statement (Lean)
159theorem voice_forcing_chain : True := trivial
proof body
Term-mode proof.
160
161end
162
163/-! ## Summary -/
164