На самом деле, проще непосредственно подсказать суждение о подсети.Тем не менее, вы должны быть максимально общими, поэтому вот мой совет:
Lemma proof1: forall (A:Type) (x:A) (l1 l2:list A),
SubSeq l1 l2 -> InL x l1 -> InL x l2.
(* first introduce your hypothesis, but put back x and In foo
inside the goal, so that your induction hypothesis are correct*)
intros.
revert x H0. induction H; intros.
(* x In [] is not possible, so inversion will kill the subgoal *)
inversion H0.
(* here it is straitforward: just combine the correct hypothesis *)
apply InTail; apply IHSubSeq; trivial.
(* x0 in x::l1 has to possible sources: x0 == x or x0 in l1 *)
inversion H0; subst; clear H0.
apply InHead.
apply InTail; apply IHSubSeq; trivial.
Qed.
«инверсия» - это тактика, которая проверяет индуктивный термин и дает вам все возможные способы построения такого термина!без всякой индукционной гипотезы !!Это дает вам только конструктивные предпосылки.
Вы могли бы сделать это напрямую, индуцируя по l1, затем по l2, но вам пришлось бы вручную построить правильный пример инверсии, потому что ваша гипотеза индукции была бы действительно слабой.
Надеюсь, это поможет, V.