'Cegar.solve_safe_iff' depends on axioms: [propext, Quot.sound]
'Cegar.safe_of_may_safe' depends on axioms: [propext, Quot.sound]
'Cegar.Lift.nodes' depends on axioms: [propext]
'Cegar.lift_of_nodes' depends on axioms: [propext]
'Cegar.tabulate' depends on axioms: [propext, Quot.sound]
'Cegar.checkBad' depends on axioms: [propext, Quot.sound]
'Cegar.cut_refines' depends on axioms: [propext, Quot.sound]
'Cegar.cut_shorter' depends on axioms: [propext, Quot.sound]
'Cegar.cut_eliminates' depends on axioms: [propext, Quot.sound]
'Cegar.run' depends on axioms: [propext, Quot.sound]
'Cegar.run_safe_iff' depends on axioms: [propext, Quot.sound]
'Cegar.Logic.reflects' depends on axioms: [propext, Quot.sound]
'Cegar.Logic.rename_denote' depends on axioms: [propext, Quot.sound]
'Cegar.Layered.conditions_reflect' depends on axioms: [propext, Quot.sound]
'Cegar.Layered.check_reflect' depends on axioms: [propext, Quot.sound]
'Cegar.Layered.check_sound' depends on axioms: [propext, Quot.sound]
