We introduce a lemma.
Lemma test : forall x, x -> x.
1 subgoal ============================ forall x : Type, x -> x
We start proving it.
intros.
1 subgoal x : Type X : x ============================ x
We continue.
auto.
No more subgoals.
We end. We show the result.
Print test.
test = fun (x : Type) (X : x) => X : forall x : Type, x -> x Argument scopes are [type_scope _]