proposition: Lemma fold_inject `{Monoid A}: fold sq ∘ inject A = id.
proof: Proof. apply (sequence_extend_commutes sq id). apply _. Qed.
imports: MathClasses.theory.categories MathClasses.interfaces.functors MathClasses.interfaces.abstract_algebra MathClasses.interfaces.sequences