Theorem: LO.Modal.Standard.DeductionParameterRules.henkin_le (Logic/Modal/Standard/Deduction.lean)

State before:
α : Type u_1
inst✝ : DecidableEq α
R₁ R₂ : DeductionParameterRules
h : autoParam (R₁ ≤ R₂) _auto✝
hHenkin : R₁.henkin = true
⊢ R₂.henkin = true
Tactic:
apply h.2.2
State after:
α : Type u_1
inst✝ : DecidableEq α
R₁ R₂ : DeductionParameterRules
h : autoParam (R₁ ≤ R₂) _auto✝
hHenkin : R₁.henkin = true
⊢ R₁.henkin = true

State before:
α : Type u_1
inst✝ : DecidableEq α
R₁ R₂ : DeductionParameterRules
h : autoParam (R₁ ≤ R₂) _auto✝
hHenkin : R₁.henkin = true
⊢ R₁.henkin = true
Tactic:
assumption
State after:
no goals