# How to correctly feed type argument in this toy theorem?

I have a recursive function combine defined as following:

Fixpoint combine {X Y : Type} (lx : list X) (ly : list Y)
: list (X*Y) :=
match lx, ly with
| [], _ => []
| _, [] => []
| x :: tx, y :: ty => (x, y) :: (combine tx ty)
end.


Where list is defined as:

Inductive list (X:Type) : Type :=
| nil
| cons (x : X) (l : list X).


then I tried to define a lemma that looks like this:

Lemma list_nil_imply_combine_nil: forall {X: Type} (l: list X),
l = [] -> combine l [] = [].


but when executing the Lemma definition, Output says:

Cannot infer the implicit parameter Y of combine whose type is
"Type" in environment:
X : Type
l : list X


I'm not sure how to correctly feed type arguments to [] i.e. nil constructor.. Any hint or direction for help material is appreciated!

Lemma list_nil_imply_combine_nil: forall {X Y: Type} (l: list X),
combine l ([] : list Y) = [].


?

Anyway, a solution is to explicitly give the type of [], which is enough to help Coq find the type argument by itself:

Lemma list_nil_imply_combine_nil: forall {X Y: Type} (l: list X),
combine l ([] : list Y) = [].


Another is to feed the argument yourself, like so:

Lemma list_nil_imply_combine_nil: forall {X Y: Type} (l: list X),
combine l (@nil Y) = [].


The use of @ locally deactivates the implicit arguments, letting you give all arguments.

you need to type the nil :

Lemma list_nil_imply_combine_nil: forall {X Y : Type} (l: list X),
l = [] -> combine l ([] : list Y) = [].