Goal True /\ True.
Proof.
  split.
  par:exact I.
Qed.