'MarginRatioTwo.half_b2_lower' depends on axioms: [propext, Classical.choice, Quot.sound]
'MarginRatioTwo.half_b2_upper' depends on axioms: [propext, Classical.choice, Quot.sound]
'MarginRatioTwo.ball_bound_value' depends on axioms: [propext, Classical.choice, Quot.sound]
'MarginRatioTwo.ball_c022' depends on axioms: [propext, Classical.choice, Quot.sound]
'MarginRatioTwo.ball_c04_fails_beta28' depends on axioms: [propext, Classical.choice, Quot.sound]
'MarginRatioTwo.ball_c04' depends on axioms: [propext, Classical.choice, Quot.sound]
'MarginRatioTwo.margin2_beta28_c022' depends on axioms: [propext, Classical.choice, Quot.sound]
'MarginRatioTwo.margin2_c04_fform_fails' depends on axioms: [propext, Classical.choice, Quot.sound]
'MarginRatioTwo.margin2_ker_beta28_c022' depends on axioms: [propext, Classical.choice, Quot.sound]
'MarginRatioTwo.margin2_ker_beta54_c04' depends on axioms: [propext, Classical.choice, Quot.sound]
'MarginRatioTwo.margin2_ker_beta40_c04_fails' depends on axioms: [propext, Classical.choice, Quot.sound]
'KernelMarginStages.window_necessary' depends on axioms: [propext, Classical.choice, Quot.sound]
'KernelMarginStages.window_sufficient' depends on axioms: [propext, Classical.choice, Quot.sound]
'KernelMarginStages.window_beta28_fails_tau1' depends on axioms: [propext, Classical.choice, Quot.sound]
'KernelMarginStages.window_beta28_fails_tau3' depends on axioms: [propext, Classical.choice, Quot.sound]
'KernelMarginStages.window_33_tau1_l0' depends on axioms: [propext, Classical.choice, Quot.sound]
'KernelMarginStages.window_33_tau3_l0' depends on axioms: [propext, Classical.choice, Quot.sound]
'KernelMarginStages.window_33_tau3_l16_fails' depends on axioms: [propext, Classical.choice, Quot.sound]
'KernelMarginStages.window_36_tau1_l16_fails' depends on axioms: [propext, Classical.choice, Quot.sound]
'KernelMarginStages.window_36_tau3_l16' depends on axioms: [propext, Classical.choice, Quot.sound]
'KernelMarginStages.window_38_tau1_l16' depends on axioms: [propext, Classical.choice, Quot.sound]
'KernelMarginStages.window_38_tau3_l36_fails' depends on axioms: [propext, Classical.choice, Quot.sound]
'KernelMarginStages.one_sub_lambda' depends on axioms: [propext, Classical.choice, Quot.sound]
'KernelMarginStages.margin_of' depends on axioms: [propext, Classical.choice, Quot.sound]
'KernelMarginStages.margin_33_tau1_l0' depends on axioms: [propext, Classical.choice, Quot.sound]
'KernelMarginStages.margin_33_tau3_l0' depends on axioms: [propext, Classical.choice, Quot.sound]
'KernelMarginStages.margin_36_tau1_l0' depends on axioms: [propext, Classical.choice, Quot.sound]
'KernelMarginStages.margin_36_tau3_l0' depends on axioms: [propext, Classical.choice, Quot.sound]
'KernelMarginStages.margin_36_tau3_l16' depends on axioms: [propext, Classical.choice, Quot.sound]
'KernelMarginStages.margin_38_tau1_l0' depends on axioms: [propext, Classical.choice, Quot.sound]
'KernelMarginStages.margin_38_tau1_l16' depends on axioms: [propext, Classical.choice, Quot.sound]
'KernelMarginStages.margin_38_tau3_l0' depends on axioms: [propext, Classical.choice, Quot.sound]
'KernelMarginStages.margin_38_tau3_l16' depends on axioms: [propext, Classical.choice, Quot.sound]
'KernelWindowTable.window_30_tau1_l0_fails' depends on axioms: [propext, Classical.choice, Quot.sound]
'KernelWindowTable.window_30_tau3_l0' depends on axioms: [propext, Classical.choice, Quot.sound]
'KernelWindowTable.window_43_tau1_l36' depends on axioms: [propext, Classical.choice, Quot.sound]
'KernelWindowTable.window_54_tau1_l36' depends on axioms: [propext, Classical.choice, Quot.sound]
'KernelWindowTable.window_38_tau1_l36_fails' depends on axioms: [propext, Classical.choice, Quot.sound]
'KernelWindowTable.window_36_tau1_l16_fails'' depends on axioms: [propext, Classical.choice, Quot.sound]
'KernelWindowTable.margin_30_tau3_l0' depends on axioms: [propext, Classical.choice, Quot.sound]
'KernelWindowTable.margin_43_tau1_l36' depends on axioms: [propext, Classical.choice, Quot.sound]
'KernelWindowTable.margin_54_tau1_l36' depends on axioms: [propext, Classical.choice, Quot.sound]
'KernelWindowTable.measured_inside' depends on axioms: [propext, Classical.choice, Quot.sound]
