Supporting results for pointwise provable equality.

Hilbert-Bernays-Löb derivability condition $\mathbf{D2}$

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.modus_ponens {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {L : Language} [L.Encodable] [L.LORDefinable] (T : Theory L) [T.Δ₁] {φ ψ : Proposition L} (hφψ : Provable T ⌜φ ⇒ₗ ψ⌝) (hφ : Provable T ⌜φ⌝) : Provable T ⌜ψ⌝

Hilbert–Bernays provability condition D2

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.modus_ponens_sentence {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {L : Language} [L.Encodable] [L.LORDefinable] (T : Theory L) [T.Δ₁] {σ τ : Sentence L} (hστ : Provable T ⌜σ ⇒ₗ τ⌝) (hσ : Provable T ⌜σ⌝) : Provable T ⌜τ⌝