'Erdos796.extractedTailGate_proved' depends on axioms: [propext, Classical.choice, Quot.sound]
'Erdos796.erdos796_statement' depends on axioms: [propext, Classical.choice, Quot.sound]
