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