intro f g h f_is_g g_is_h W M w
⊢ ∀ ⦃x y z : Formula⦄,
    (∀ (W : Type) (M : KripkeModel W) (w : W), evaluate M w x ↔ evaluate M w y) →
      (∀ (W : Type) (M : KripkeModel W) (w : W), evaluate M w y ↔ evaluate M w z) →
        ∀ (W : Type) (M : KripkeModel W) (w : W), evaluate M w x ↔ evaluate M w z
f g h : Formula
f_is_g : ∀ (W : Type) (M : KripkeModel W) (w : W), evaluate M w f ↔ evaluate M w g
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
⊢ evaluate M w f ↔ evaluate M w h