'CliffordSmall.qi_sq' depends on axioms: [propext, Classical.choice, Quot.sound]
'CliffordSmall.qj_sq' depends on axioms: [propext, Classical.choice, Quot.sound]
'CliffordSmall.qi_qj_anticomm' depends on axioms: [propext, Classical.choice, Quot.sound]
'CliffordSmall.J_sq' depends on axioms: [propext, Classical.choice, Quot.sound]
'CliffordSmall.J_det' depends on axioms: [propext, Classical.choice, Quot.sound]