6 lines
No EOL
104 B
Coq
6 lines
No EOL
104 B
Coq
Require Export UniMath.Foundations.All.
|
|
|
|
Lemma myfirstlemma : 2 + 2 = 4.
|
|
Proof.
|
|
apply idpath.
|
|
Defined. |