theorem
proved
term proof
cert_inhabited
show as:
view Lean formalization →
formal statement (Lean)
189theorem cert_inhabited : Nonempty PreTemporalOrderCert := ⟨cert⟩
proof body
Term-mode proof.
190
191end PreTemporalForcingOrder
192end Foundation
193end IndisputableMonolith