Hola Agustin.
Para probar una propiedad sobre una función recursiva, definida sobre al menos un parámetro definido inductivamente, te sugiero (como se vio en el teórico) seguir la lógica de la función para plantear los casos de la prueba. En particular, si una función se define recursivamete sobre cierto parámetro, es conviente hacer inducción sobre éste; de esta manera podrás aplicar la definición de la función (el conocimiento de ésta), en general con la táctica simpl. Si en algún caso la función hace análisis de casos, lo mismo te conviene hacer a nivel de la prueba, para ir probarndo los casos siguiendo la definción de la función.
Por ejemplo, vemos una propiedad sobre la función sum entre naturales, definida recursicamente sobre su primer argumento:
Fixpoint sum (n m: nat) {struct n}: nat :=
match n with
| 0 => m
| S k => S (sum k m)
end.
(* Ej 9.2 *)
Lemma SumS : forall n m : nat, sum n (S m) = sum (S n) m.
Proof.
intros n m.
induction n; simpl.
(* aplico inducción en el parámetro de sum sobre el cual se hace recursión y luego simplifico según la definición de sum *)
reflexivity.
rewrite -> IHn; simpl.
(* aplico la hipótesis inductiva y nuevamente simplifico según la definción de sum *)
reflexivity.
Qed.
Saludos, Carlos