exact ⟨StrongCut.cut H.get b⟩
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
no goals