Theorem: LeanSAT.Encode.ofList_eq_map_get (LeanSAT/Encode/Card.lean)

State before:
α : Type u_1
L : List α
⊢ ↑L = Multiset.map (fun i => List.get L i) Finset.univ.val
Tactic:
conv => lhs; rw [← List.finRange_map_get (l := L)]
State after:
no goals