theorem proved term proof

`constant_not_recognizer`

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

formal statement (Lean)

 115theorem constant_not_recognizer (C : Type*) [Nonempty C] (e : E) :
 116    ¬∃ c₁ c₂ : C, (fun _ : C => e) c₁ ≠ (fun _ : C => e) c₂ := by

Term-mode proof.

 117  push_neg
 118  intros
 119  rfl
 120
 121/-! ## Module Status -/
 122

Lean names referenced from this declaration's body.