Goal True /\ True.
split.
- exact I.
- exact I.
Qed.