1 2 3 4 5 6 7 8 9 10 11 12
Section Foo. Variable A : Type. Definition bla := A. Variable B : bla. Lemma blu : {X:Type & X}. Proof using A B. exists bla;exact B. Qed. End Foo.