no goals
α : Type u_1
β : Type ?u.135359
γ : Type ?u.135362
dec : DecidableEq α
a b : α
R S : RegularExpression α
⊢ map id (R + S) = R + S
simp_rw [map, map_id]
no goals
α : Type u_1
β : Type ?u.135359
γ : Type ?u.135362
dec : DecidableEq α
a b : α
R S : RegularExpression α
⊢ map id (R * S) = R * S
simp_rw [map, map_id]
no goals
α : Type u_1
β : Type ?u.135359
γ : Type ?u.135362
dec : DecidableEq α
a b : α
R : RegularExpression α
⊢ map id (star R) = star R
simp_rw [map, map_id]