I have the defined inductive types:
Inductive InL (A:Type) (y:A) : list A -> Prop :=
| InHead : forall xs:list A, InL y (cons y xs)
| InTail : forall (x:A) (xs:list A), InL y xs -> InL y (cons x xs).
Inductive SubSeq (A:Type) : list A -> list A -> Prop :=
| SubNil : forall l:list A, SubSeq nil l
| SubCons1 : forall (x:A) (l1 l2:list A), SubSeq l1 l2 -> SubSeq l1 (x::l2)
| SubCons2 : forall (x:A) (l1 l2:list A), SubSeq l1 l2 -> SubSeq (x::l1) (x::l2).
Now I have to prove a series of properties of that inductive type, but I keep getting stuck.
Lemma proof1: forall (A:Type) (x:A) (l1 l2:list A), SubSeq l1 l2 -> InL x l1 -> InL x l2.
Proof.
intros.
induction l1.
induction l2.
exact H0.
Qed.
Can some one help me advance.
In fact, it is easier to do an induction on the SubSet judgment directly. However, you need to be as general as possible, so here is my advice:
"inversion" is a tactic that checks an inductive term and gives you all the possible way to build such a term !!without any induction hypothesis!! It only gives you the constructive premices.
You could have done it directly by induction on l1 then l2, but you would have to construct by hand the correct instance of inversion because your induction hypothesis would have been really weak.
Hope it helps, V.