Require Export UniMath.Foundations.All.

Lemma myfirstlemma : 2 + 2 = 4.
Proof.
  apply idpath.
Defined.