Set type Variable to a concrete type inside a definition

Say that we define in Coq:

Section bin_trees.

Variable T: Type.

Inductive bin_tree :=
  | Leaf : bin_tree
  | Node : T ->  bin_tree -> bin_tree -> bin_tree.

Within bin_trees section, I would like to define some sample tree:

Definition my_nat_bin_tree := Node 3 Leaf Leaf.

But this is not allowed:

Error: In environment
T : Type
The term "3" has type "nat"
while it is expected to have type 
"T".

Can I set T to some concrete type (in this case nat) for the purposes of a single definition? Something like:

Definition my_nat_bin_tree := @Node (T:=nat) 3 Leaf Leaf.

Or maybe there is a trick to close and reopen the section after the definitions so that I can refer to T variable without redeclaring it?

You probably want to close the section anyway. But that does not mean you have to provide an explicit T everywhere.

This code shows how to use the Arguments command to make T implicit.

Section bin_trees.
Variable T : Type.
Inductive bin_tree :=
  | Leaf : bin_tree
  | Node : T ->  bin_tree -> bin_tree -> bin_tree.
End bin_trees.

(* Outside the section, T is a parameter for Leaf, Node and bin_tree. *)
Check Leaf : forall T : Type, bin_tree T.
Check Node : forall T : Type, T -> bin_tree T -> bin_tree T -> bin_tree T.

(* You can tell coq to deduce T from the context. *)
Arguments Node {T}.
Arguments Leaf {T}.

(* Since 3 is in nat, there is no other choice for T. *)
Definition my_nat_bin_tree := Node 3 Leaf Leaf.
Check my_nat_bin_tree : bin_tree nat.

Definition my_bool_bin_tree := Node false (Node true Leaf Leaf) Leaf.
Check my_bool_bin_tree : bin_tree bool.

(* Now if one really wants some Leaf of type, say nat *)
Fail Definition my_nat_leaf := Leaf. (* does not work :
- ?T: Cannot infer the implicit parameter T of Leaf whose type is "Type". *)
(* But we can "unexplicit" T locally with the @ operator *)
Definition my_nat_leaf := @Leaf nat.
Check my_nat_leaf : bin_tree nat.

About the section, actually if T is not that much used you can also directly give the type as a parameter as in :

Inductive bin_tree' (T : Type) :=
  | Leaf' : bin_tree' T
  | Node' : T ->  bin_tree' T -> bin_tree' T -> bin_tree' T.

A trick you can use is to use notation to locally instanciate a definition.

Section Top.

Inductive bin_tree (T : Type) :=
  | Leaf : bin_tree T
  | Node : T ->  bin_tree T -> bin_tree T -> bin_tree T.

Section bin_trees.

Variable T : Type.

Notation bin_tree := (bin_tree T).
Notation Leaf := (Leaf T).
Notation Node := (Node T).

Check bin_tree.
Check Leaf.
Check Node.

Definition my_nat_bin_tree := Top.Node _ 3 (Top.Leaf _) (Top.Leaf _).

Print my_nat_bin_tree.

End bin_trees.

Print my_nat_bin_tree.

End Top.

Print my_nat_bin_tree.