1 2 3 4 5 6 7 8
Section Foo. Variable A : Type. Lemma foo : A -> True. now intros _. Qed. Goal Type -> True. rename A into B. intros A. Fail apply foo.