lemma proved term proof

`trivial_hasCover`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

  37lemma trivial_hasCover : HasCover trivialInstance := by

Term-mode proof.

  38  refine ⟨[], by decide, ?_⟩
  39  intro e he
  40  simpa using he
  41

Lean names referenced from this declaration's body.