theorem
SimpleRewrites.Equation613_implies_Equation608
(G : Type u_1)
[Magma G]
(h : Equation613 G)
:
theorem
SimpleRewrites.Equation816_implies_Equation811
(G : Type u_1)
[Magma G]
(h : Equation816 G)
:
theorem
SimpleRewrites.Equation1019_implies_Equation1014
(G : Type u_1)
[Magma G]
(h : Equation1019 G)
:
theorem
SimpleRewrites.Equation1222_implies_Equation1217
(G : Type u_1)
[Magma G]
(h : Equation1222 G)
:
theorem
SimpleRewrites.Equation1425_implies_Equation1420
(G : Type u_1)
[Magma G]
(h : Equation1425 G)
:
theorem
SimpleRewrites.Equation1628_implies_Equation1623
(G : Type u_1)
[Magma G]
(h : Equation1628 G)
:
theorem
SimpleRewrites.Equation1831_implies_Equation1826
(G : Type u_1)
[Magma G]
(h : Equation1831 G)
:
theorem
SimpleRewrites.Equation2034_implies_Equation2029
(G : Type u_1)
[Magma G]
(h : Equation2034 G)
:
theorem
SimpleRewrites.Equation2237_implies_Equation2232
(G : Type u_1)
[Magma G]
(h : Equation2237 G)
:
theorem
SimpleRewrites.Equation2440_implies_Equation2435
(G : Type u_1)
[Magma G]
(h : Equation2440 G)
:
theorem
SimpleRewrites.Equation2643_implies_Equation2638
(G : Type u_1)
[Magma G]
(h : Equation2643 G)
:
theorem
SimpleRewrites.Equation2846_implies_Equation2841
(G : Type u_1)
[Magma G]
(h : Equation2846 G)
:
theorem
SimpleRewrites.Equation3049_implies_Equation3044
(G : Type u_1)
[Magma G]
(h : Equation3049 G)
:
theorem
SimpleRewrites.Equation3252_implies_Equation3247
(G : Type u_1)
[Magma G]
(h : Equation3252 G)
:
theorem
SimpleRewrites.Equation3455_implies_Equation3450
(G : Type u_1)
[Magma G]
(h : Equation3455 G)
:
theorem
SimpleRewrites.Equation3658_implies_Equation3653
(G : Type u_1)
[Magma G]
(h : Equation3658 G)
:
theorem
SimpleRewrites.Equation3861_implies_Equation3856
(G : Type u_1)
[Magma G]
(h : Equation3861 G)
:
theorem
SimpleRewrites.Equation4064_implies_Equation4059
(G : Type u_1)
[Magma G]
(h : Equation4064 G)
:
theorem
SimpleRewrites.Equation4267_implies_Equation4262
(G : Type u_1)
[Magma G]
(h : Equation4267 G)
:
theorem
SimpleRewrites.Equation4582_implies_Equation4577
(G : Type u_1)
[Magma G]
(h : Equation4582 G)
: