Theorem: LO.System.StrongCut.cut! (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✝² : Collection F T
inst✝¹ : Axiomatized S
inst✝ : StrongCut S T
𝓢 : S
𝓣 : T
p : F
H : 𝓢 ⊢!* Collection.set 𝓣
hp : 𝓣 ⊢! p
⊢ 𝓢 ⊢! p
Tactic:
rcases hp with ⟨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✝² : Collection F T
inst✝¹ : Axiomatized S
inst✝ : StrongCut S T
𝓢 : S
𝓣 : T
p : F
H : 𝓢 ⊢!* Collection.set 𝓣
b : 𝓣 ⊢ p
⊢ 𝓢 ⊢! p

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✝² : Collection F T
inst✝¹ : Axiomatized S
inst✝ : StrongCut S T
𝓢 : S
𝓣 : T
p : F
H : 𝓢 ⊢!* Collection.set 𝓣
b : 𝓣 ⊢ p
⊢ 𝓢 ⊢! p
Tactic:
exact ⟨StrongCut.cut H.get b⟩
State after:
no goals