theorem SimpleRewrites.Equation3455_implies_Equation3450 (G : Type u_1) [Magma G] (h : Equation3455 G) : Equation3450 G

theorem SimpleRewrites.Equation3658_implies_Equation3653 (G : Type u_1) [Magma G] (h : Equation3658 G) : Equation3653 G

theorem SimpleRewrites.Equation4064_implies_Equation4059 (G : Type u_1) [Magma G] (h : Equation4064 G) : Equation4059 G