proposition: Lemma twist : forall x y z t:U, cong (op x (op (op y z) t)) (op (op y (op x t)) z).
proof: Proof. intros. apply cong_trans with (op x (op (op y t) z)). - apply cong_right; apply perm_right. - apply cong_trans with (op (op x (op y t)) z). + apply cong_sym; apply op_ass. + apply cong_left; apply perm_left. Qed.