Theorem: BoolExpr.map_fin_val_attach_go (LeanSAT/Reflect/BoolExpr/Decidable.lean)

State before:
x : BoolExpr Nat
k : Nat
h : x.vars ≤ k
⊢ map Fin.val (attach.go x k h) = x
Tactic:
cases x <;> simp [attach.go, map, map_fin_val_attach_go]
State after:
no goals