title: How to apply a constructor in an hypothesis?
body: <p>I am trying to prove the following theorem</p>
  <pre><code>Theorem subseq_subset : forall l1 l2, subseq l1 l2 -&gt; sublist l1 l2.
  </code></pre>
  <p>with  the inductive type subseq :</p>
  <pre><code>Inductive subseq {A:Type} : list A -&gt; list A -&gt; Prop :=
  | SubNil   : forall (l:list A), subseq  nil l
  | Sub_both : forall (s l:list A) (x:A), subseq  s l -&gt; subseq s (x::l)
  | Sub_right : forall (s l: list A) (x:A), subseq s l -&gt; subseq (x::s) (x::l). 
  </code></pre>
  <p>and the definition of sublist:</p>
  <pre><code> Definition sublist (l1 l2 : list A) : Prop := forall x : A, In x l1 -&gt; In x l2.
  </code></pre>
  <p>this is the proof i started to do</p>
  <pre><code>Theorem subseq_subset : forall l1 l2, subseq l1 l2 -&gt; sublist l1 l2.
  Proof.
  intros.
  
  unfold sublist. intros.
  induction l2.
  + inversion H in H0. simpl. simpl in H0. assumption.
  + apply in_cons. apply IHl2.
  Qed.
  </code></pre>
  <p>i have this context now</p>
  <pre><code>1 subgoals
  l1 : list A
  a : A
  l2 : list A
  H : subseq l1 (a :: l2)
  x : A
  H0 : In x l1
  IHl2 : subseq l1 l2 -&gt; In x l2
  ______________________________________(1/1)
  subseq l1 l2
  </code></pre>
  <p>i thought to apply sub_right on H so i can end the proof with assumption but <code>apply sub_right in H</code> is not working. Is this possible? and how can i end this proof?</p>
  <p>Thanks.</p>