theorem SimpleRewrites.Equation613_implies_Equation612 (G : Type u_1) [Magma G] (h : Equation613 G) : Equation612 G

theorem SimpleRewrites.Equation816_implies_Equation815 (G : Type u_1) [Magma G] (h : Equation816 G) : Equation815 G

theorem SimpleRewrites.Equation1019_implies_Equation1018 (G : Type u_1) [Magma G] (h : Equation1019 G) : Equation1018 G

theorem SimpleRewrites.Equation1222_implies_Equation1221 (G : Type u_1) [Magma G] (h : Equation1222 G) : Equation1221 G

theorem SimpleRewrites.Equation1425_implies_Equation1424 (G : Type u_1) [Magma G] (h : Equation1425 G) : Equation1424 G

theorem SimpleRewrites.Equation1628_implies_Equation1627 (G : Type u_1) [Magma G] (h : Equation1628 G) : Equation1627 G

theorem SimpleRewrites.Equation1831_implies_Equation1830 (G : Type u_1) [Magma G] (h : Equation1831 G) : Equation1830 G

theorem SimpleRewrites.Equation2034_implies_Equation2033 (G : Type u_1) [Magma G] (h : Equation2034 G) : Equation2033 G

theorem SimpleRewrites.Equation2237_implies_Equation2236 (G : Type u_1) [Magma G] (h : Equation2237 G) : Equation2236 G

theorem SimpleRewrites.Equation2643_implies_Equation2642 (G : Type u_1) [Magma G] (h : Equation2643 G) : Equation2642 G

theorem SimpleRewrites.Equation2846_implies_Equation2845 (G : Type u_1) [Magma G] (h : Equation2846 G) : Equation2845 G

theorem SimpleRewrites.Equation3049_implies_Equation3048 (G : Type u_1) [Magma G] (h : Equation3049 G) : Equation3048 G

theorem SimpleRewrites.Equation3252_implies_Equation3251 (G : Type u_1) [Magma G] (h : Equation3252 G) : Equation3251 G