(* proofs of permutation lemma for two premise logical rules *) P2Rotate = CRotate + Merge_Msde