§
Check Lean Discrimination Tree Indexing
use:
#discr_tree_simp_key extractLsb'_eq_self