Theorem: Metamath.HH_cons (Metamath/Translate.lean)

State before:
axs : Statement → Prop
Γ : Context
σ : VR → Expr
c : CN
f : Expr
hyps : List (CN × Expr)
e : Expr
inst✝ : Subst σ f e
h₁ : Provable axs Γ (c, e)
h₂ : ∀ (h : Formula), h ∈ hyps → Provable axs Γ (Formula.subst σ h)
⊢ Provable axs Γ (Formula.subst σ (c, f))
Tactic:
rw [← @Subst.out σ f e] at h₁
State after:
axs : Statement → Prop
Γ : Context
σ : VR → Expr
c : CN
f : Expr
hyps : List (CN × Expr)
e : Expr
inst✝ : Subst σ f e
h₁ : Provable axs Γ (c, Expr.subst σ f)
h₂ : ∀ (h : Formula), h ∈ hyps → Provable axs Γ (Formula.subst σ h)
⊢ Provable axs Γ (Formula.subst σ (c, f))

State before:
axs : Statement → Prop
Γ : Context
σ : VR → Expr
c : CN
f : Expr
hyps : List (CN × Expr)
e : Expr
inst✝ : Subst σ f e
h₁ : Provable axs Γ (c, Expr.subst σ f)
h₂ : ∀ (h : Formula), h ∈ hyps → Provable axs Γ (Formula.subst σ h)
⊢ Provable axs Γ (Formula.subst σ (c, f))
Tactic:
exact h₁
State after:
no goals