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