simp [h.theory_eq, h'.theory_eq]
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
𝓢 𝓣 : S
h : Inconsistent 𝓢
h' : Inconsistent 𝓣
f : F
⊢ f ∈ theory 𝓢 ↔ f ∈ theory 𝓣
no goals