Theorem bool.or_of_bor_eq

feat(*): working on list/basic, robusting simp proofs

refactor(*): attributes on same line

refactor(*): import content from lean/library/data and library_dev