Unprovable flon

lemma unprovable_flon [consis : Consistent T] [𝔅.FormalizedCompleteOn 𝐉] : T ⊬ flon 𝔅 𝔚 := by  contrapose! consis;  replace consis : T ⊢ ∀¹ safe 𝔅 𝔚 := by simpa [flon] using consis;  have h₁ : T ⊢ ∼(𝔅 𝐉 ⋏ 𝔚 𝐉) := by simpa [safe] using! FirstOrder.Theory.Proof.specialize _ _ ⨀ consis;  have h₂ : T ⊢ ∼𝐉 := (contra! jeroslow_not_safe) ⨀ h₁;  have h₃ : T ⊢ 𝐉 🡘 𝔚 𝐉 := jeroslow_def';  have h₄ : T ⊢ 𝔚 𝐉 := R1' h₂;  have h₅ : T ⊢ 𝔚 𝐉 🡒 𝐉 := by cl_prover [h₃];  have h₆ : T ⊢ 𝐉 := h₅ ⨀ h₄;  exact not_consistent_iff_inconsistent.mpr <| inconsistent_iff_provable_bot.mpr $ (N!_iff_CO!.mp h₂) ⨀ h₆;