simp [System.inconsistent_iff_provable_bot]
L₁ : Language
L₂ : Language
L : Language
T✝ : Theory L
Γ Δ : Sequent L
Φ : L₁ →ᵥ L₂
T : Theory L₁
⊢ System.Inconsistent T → System.Inconsistent (Theory.lMap Φ T)
L₁ : Language
L₂ : Language
L : Language
T✝ : Theory L
Γ Δ : Sequent L
Φ : L₁ →ᵥ L₂
T : Theory L₁
⊢ T ⊢! ⊥ → Theory.lMap Φ T ⊢! ⊥