'IndisputableMonolith.Foundation.TraceRealization.AppendRetention.encoder_classification' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'IndisputableMonolith.Foundation.TraceRealization.AppendRetention.encoder_faithful_iff' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'IndisputableMonolith.Foundation.TraceRealization.AppendRetention.double_charge_faithful' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'IndisputableMonolith.Foundation.TraceRealization.AppendRetention.concatenateTurns_deform' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'IndisputableMonolith.Foundation.TraceRealization.AppendRetention.recover_concatenate_iff_same_sign' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'IndisputableMonolith.Foundation.TraceRealization.AppendRetention.admissible_set_lies_in_one_cone' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'IndisputableMonolith.Foundation.TraceRealization.AppendRetention.additive_nonnegative_readout_zero' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'IndisputableMonolith.Foundation.TraceRealization.AppendRetention.no_global_append_decoder' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]