∀ {R : Type u_2} {S : Type u_1} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (motive :
    (Subsingleton (Algebra.H1Cotangent R S) ∧ ∃ I b, Set.range ⇑b ⊆ Set.range ⇑(KaehlerDifferential.D R S)) → Prop)
  (x : Subsingleton (Algebra.H1Cotangent R S) ∧ ∃ I b, Set.range ⇑b ⊆ Set.range ⇑(KaehlerDifferential.D R S)),
  (∀ (h : Subsingleton (Algebra.H1Cotangent R S)) (w : Type) (b : Module.Basis w S Ω[S⁄R])
      (hb : Set.range ⇑b ⊆ Set.range ⇑(KaehlerDifferential.D R S)), motive ⋯) →
    motive x