blob: 5260b7cdafd2252062b9cedfadcfe839ba81bd7d (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
|
Require Import A B.
Definition z := x + y.
Lemma zeq : z = z.
Proof. pose xeq. pose yeq. auto. Qed.
Lemma yeq'' : y = y.
Proof. apply yeq'. Admitted.
Module M. Include B.M. End M.
Module T. Include B.T. End T.
Module F. Include B.F. End F.
|
