Theorem: LO.System.Deduction.inv! (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 : 𝓢 ⊢! p ⟶ q
⊢ cons 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 : 𝓢 ⊢ p ⟶ q
⊢ cons 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 : 𝓢 ⊢ p ⟶ q
⊢ cons p 𝓢 ⊢! q
Tactic:
exact ⟨Deduction.inv b⟩
State after:
no goals