theorem proved term proof

`reverse_involution`

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

formal statement (Lean)

  38theorem reverse_involution (k : Fin 8) : reverse (reverse k) = k := by

Term-mode proof.

  39  apply Fin.ext
  40  simp only [reverse]
  41  omega
  42
  43/-- Reversal swaps first and last. -/

From the project-wide theorem graph. These declarations reference this one in their body.

developmentReversalCert in IndisputableMonolith.CrossDomain.DevelopmentReversal decl_use

Lean names referenced from this declaration's body.