∀ (K L : Type) [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] [FiniteDimensional K L]
  (x : ↥(groupCohomology.cocycles₁ (Rep.ofAlgebraAutOnUnits K L))),
  ⇑x ∈ groupCohomology.coboundaries₁ (Rep.ofAlgebraAutOnUnits K L)