IndisputableMonolith.Gravity.SevenGaps.Gap2FugacityEliminationHostileProbe

declarations in this module (12)

• theorem a14_class_inhabited_by_unit_character L26
• theorem gibbsSize_witnesses_unit_fugacity L45
• theorem witness_tilted_posts_mu_and_not_sizeWeight L50
• theorem witness_characterCost_continuum L64
• theorem witness_surfaceCost_escapes_kindTotals L78
• theorem thm3_first_conjunct_is_hypothesis_free L96
• theorem thm3_load_bearing_is_a17 L100
• theorem a17_lands_ignores_binders L112
• theorem full_posting_force_is_pointwise L120
• theorem thm1_is_a14_alias L133
• theorem flag_unmoved_rfl L145
• theorem ledger_gap2_now_true L149