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.Equation2440_implies_Equation2439 (G : Type u_1) [Magma G] (h : Equation2440 G) : Equation2439 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

theorem SimpleRewrites.Equation3455_implies_Equation3454 (G : Type u_1) [Magma G] (h : Equation3455 G) : Equation3454 G

theorem SimpleRewrites.Equation3658_implies_Equation3657 (G : Type u_1) [Magma G] (h : Equation3658 G) : Equation3657 G

theorem SimpleRewrites.Equation3861_implies_Equation3860 (G : Type u_1) [Magma G] (h : Equation3861 G) : Equation3860 G

theorem SimpleRewrites.Equation4064_implies_Equation4063 (G : Type u_1) [Magma G] (h : Equation4064 G) : Equation4063 G

theorem SimpleRewrites.Equation4267_implies_Equation4266 (G : Type u_1) [Magma G] (h : Equation4267 G) : Equation4266 G

theorem SimpleRewrites.Equation4582_implies_Equation4581 (G : Type u_1) [Magma G] (h : Equation4582 G) : Equation4581 G