Theorem: LO.System.Axiomatized.weakening! (Logic/Logic/System.lean)

State before:
F : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
inst✝⁴ : System F S
inst✝³ : System F T
inst✝² : System F U
inst✝¹ : Collection F S
inst✝ : Axiomatized S
𝓢 𝓣 : S
h : 𝓢 ⊆ 𝓣
f : F
⊢ 𝓢 ⊢! f → 𝓣 ⊢! f
Tactic:
rintro ⟨b⟩
State after:
case intro
F : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
inst✝⁴ : System F S
inst✝³ : System F T
inst✝² : System F U
inst✝¹ : Collection F S
inst✝ : Axiomatized S
𝓢 𝓣 : S
h : 𝓢 ⊆ 𝓣
f : F
b : 𝓢 ⊢ f
⊢ 𝓣 ⊢! f

State before:
case intro
F : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
inst✝⁴ : System F S
inst✝³ : System F T
inst✝² : System F U
inst✝¹ : Collection F S
inst✝ : Axiomatized S
𝓢 𝓣 : S
h : 𝓢 ⊆ 𝓣
f : F
b : 𝓢 ⊢ f
⊢ 𝓣 ⊢! f
Tactic:
exact ⟨weakening h b⟩
State after:
no goals