theorem proved term proof

`symm`

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

formal statement (Lean)

  61theorem symm {C₁ : DisplayChannel State Obs₁} {C₂ : DisplayChannel State Obs₂}
  62    (h : QualityEquiv C₁ C₂) : QualityEquiv C₂ C₁ :=

Term-mode proof.

  63  fun x y => (h x y).symm
  64

Lean names referenced from this declaration's body.