(* Structural rule .4 for Modal logic, gives transitivity *) four = dKt + rules fours "[| $X |- @ $Y |] ==> $X |- @ @ $Y" end