Theorem: LO.System.Deduction.of_insert! (Logic/Logic/System.lean)

State before:
S : Type u_1
F : Type u_2
inst✝³ : LogicalConnective F
inst✝² : System F S
inst✝¹ : Cons F S
inst✝ : Deduction S
p q : F
𝓢 : S
h : cons p 𝓢 ⊢! q
⊢ 𝓢 ⊢! p ⟶ q
Tactic:
rcases h with ⟨b⟩
State after:
case intro
S : Type u_1
F : Type u_2
inst✝³ : LogicalConnective F
inst✝² : System F S
inst✝¹ : Cons F S
inst✝ : Deduction S
p q : F
𝓢 : S
b : cons p 𝓢 ⊢ q
⊢ 𝓢 ⊢! p ⟶ q

State before:
case intro
S : Type u_1
F : Type u_2
inst✝³ : LogicalConnective F
inst✝² : System F S
inst✝¹ : Cons F S
inst✝ : Deduction S
p q : F
𝓢 : S
b : cons p 𝓢 ⊢ q
⊢ 𝓢 ⊢! p ⟶ q
Tactic:
exact ⟨Deduction.ofInsert b⟩
State after:
no goals