lemma proved term proof

`snocBit_last`

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

formal statement (Lean)

  41@[simp] lemma snocBit_last {d : Nat} (p : Pattern d) (b : Bool) :
  42    snocBit p b (Fin.last d) = b := by

Term-mode proof.

  43  simp [snocBit]
  44
  45/-! ## The recursive BRGC path -/
  46

Lean names referenced from this declaration's body.