∀ {R : Type u1} [inst : CommRing R] {M : Type u2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {C : ExteriorAlgebra R M → Prop},
  (∀ (r : R), C ((algebraMap R (ExteriorAlgebra R M)) r)) →
    (∀ (x : M), C ((ExteriorAlgebra.ι R) x)) →
      (∀ (a b : ExteriorAlgebra R M), C a → C b → C (a * b)) →
        (∀ (a b : ExteriorAlgebra R M), C a → C b → C (a + b)) → ∀ (a : ExteriorAlgebra R M), C a