unfold semEquiv
⊢ ∀ ⦃x y z : Formula⦄, semEquiv x y → semEquiv y z → semEquiv x z
⊢ ∀ ⦃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