ci/test1.v


1
2
3
4
5
6
7
8
9
10
11
12

Definition trois := 3. (*test-definition*)
Print trois.
Eval compute in 10 * trois * trois.


Lemma easy_proof : forall A : Prop, A -> A.
Proof using .
  intros A.
  intros proof_of_A.
  exact proof_of_A.
Qed.