lemma proved term proof

`enc_true`

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

formal statement (Lean)

  16@[simp] lemma enc_true (R : Fin n → Bool) : enc (n:=n) true R = (fun i => ! (R i)) := by

Term-mode proof.

  17  funext i; simp [enc]
  18
  19/-- Restrict a full word to a queried index set `M`. -/

Lean names referenced from this declaration's body.