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 _]