specialize g_is_h W M w
f g h : Formula
g_is_h : ∀ (W : Type) (M : KripkeModel W) (w : W), Evaluate (M, w) g ↔ Evaluate (M, w) h
W : Type
M : KripkeModel W
w : W
f_is_g : Evaluate (M, w) f ↔ Evaluate (M, w) g
⊢ Evaluate (M, w) f ↔ Evaluate (M, w) h
f g h : Formula
W : Type
M : KripkeModel W
w : W
f_is_g : Evaluate (M, w) f ↔ Evaluate (M, w) g
g_is_h : Evaluate (M, w) g ↔ Evaluate (M, w) h
⊢ Evaluate (M, w) f ↔ Evaluate (M, w) h