Tengo una funcionf devolviendo un par. Entonces pruebo algunos resultados al respecto. En mis lemas, mi primer intento de obtener cada componente estaba usandolet (x, y) := f z in. Pero entonces, tratar de usar estos lemas parece engorroso.apply no funciona directamente, tengo que agregar el lema en la hipótesis usandopose proof o una variante del mismo y destruirf z para poder usarlo. ¿Hay alguna manera de usar la entrada sin problemas en las lemas? ¿O se desalienta porque es doloroso de usar?

Para completar mi pregunta, aquí están los otros intentos que hice para escribir lemas sobref. Traté de usarfst (f z) ysnd (f z) directamente, pero también lo encontré engorroso. Finalmente, comencé mis lemas conforall x y, (x,y) = f z ->.

Aquí hay un ejemplo concreto.

Require Import List. Import ListNotations.

Fixpoint split {A} (l:list A) :=
  match l with
  | [] => ([], [])
  | [a] => ([a], [])
  | a::b::l => let (l1, l2) := split l in (a::l1, b::l2)
  end.

Lemma split_in : forall {A} (l:list A) x,
  let (l1, l2) := split l in 
  In x l1 \/ In x l2 <-> In x l.

Lemma split_in2 : forall {A} (l:list A) x,
  In x (fst (split l)) \/ In x (snd (split l)) <-> In x l.

Lemma split_in3 : forall {A} (l:list A) x l1 l2,
  (l1, l2) = split l ->
  In x l1 \/ In x l2 <-> In x l.