doc-src/Ref/thm.tex

 \[ \infer[({\Imp}I)]{\phi\Imp \psi}{\infer*{\psi}{[\phi]}}  \qquad
    \infer[({\Imp}E)]{\psi}{\phi\Imp \psi & \phi}  \]
 
 \index{meta-equality}
 Equality of truth values means logical equivalence:
-\[ \infer[({\equiv}I)]{\phi\equiv\psi}{\infer*{\psi}{[\phi]} &
-                                       \infer*{\phi}{[\psi]}}  
+\[ \infer[({\equiv}I)]{\phi\equiv\psi}{\phi\Imp\psi &
+                                       \psi\Imp\phi}
    \qquad
    \infer[({\equiv}E)]{\psi}{\phi\equiv \psi & \phi}   \]
 
 The {\bf equality} rules are reflexivity, symmetry, and transitivity:
 \[ {a\equiv a}\,(refl)  \qquad