<div dir="ltr">Dear Nils,<div><br></div><div style>Thanks for the reply. Actually I got the problem solved by pattern matching as you mentioned. My complete solution is;</div><div style><br></div><div style><div style="font-family:arial,sans-serif;font-size:13.333333969116211px">
  -- Transitivity                                                                                                                                             </div><div class="im" style="font-family:arial,sans-serif;font-size:13.333333969116211px">
<div>  ⊆-trans : {A : Set}{xs ys zs : List A} → xs ⊆ ys → ys ⊆ zs → xs ⊆ zs                                                                                        </div><div>  ⊆-trans stop stop = stop                                                                                                                                    </div>
</div><div style="font-family:arial,sans-serif;font-size:13.333333969116211px">  ⊆-trans stop (drop q) = drop q                                                                                                    </div><div style="font-family:arial,sans-serif;font-size:13.333333969116211px">
  ⊆-trans p (drop q) = drop (⊆-trans p q)                                                                                                                     </div><div style="font-family:arial,sans-serif;font-size:13.333333969116211px">
  ⊆-trans (keep p) (keep q) = keep (⊆-trans p q)                                                                                                              </div><div style="font-family:arial,sans-serif;font-size:13.333333969116211px">
  ⊆-trans (drop p) (keep q) = drop (⊆-trans p q)</div><div style="font-family:arial,sans-serif;font-size:13.333333969116211px"><br></div><div style="font-family:arial,sans-serif;font-size:13.333333969116211px">Thanks</div>
<div style="font-family:arial,sans-serif;font-size:13.333333969116211px">Amila</div></div></div><div class="gmail_extra"><br><br><div class="gmail_quote">On Mon, Apr 29, 2013 at 5:36 AM, Nils Anders Danielsson <span dir="ltr">&lt;<a href="mailto:nad@cse.gu.se" target="_blank">nad@cse.gu.se</a>&gt;</span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div class="im">On 2013-04-26 03:22, Amila Jayasekara wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
I need to prove \sub is transitive. So I understand that in the<br>
transitive function I have to pattern match on stop, drop and keep<br>
cases. But I am having difficulty relating pattern matching with my<br>
proof.<br>
<br>
  ⊂-trans : {A : Set}{xs ys zs : List A} → xs ⊂ ys → ys ⊂ zs → xs ⊂ zs<br>
   ⊂-trans stop stop = stop<br>
   ⊂-trans p q with (drop p) (keep q)<br>
   ... | xs ⊂ (y :: ys) | y :: ys ⊂ y :: zs = .xs ⊂ .zs<br>
   ....<br>
   ...<br>
</blockquote>
<br></div>
There is no need to use &quot;with&quot; in this proof. As a first step you could<br>
write down the following six cases:<br>
<br>
  ⊂-trans stop     stop     = ?<br>
  ⊂-trans stop     (drop q) = ?<br>
  ⊂-trans (drop p) (drop q) = ?<br>
  ⊂-trans (drop p) (keep q) = ?<br>
  ⊂-trans (keep p) (drop q) = ?<br>
  ⊂-trans (keep p) (keep q) = ?<br>
<br>
(You can get the job done with fewer cases.)<span class="HOEnZb"><font color="#888888"><br>
<br>
-- <br>
/NAD<br>
<br>
</font></span></blockquote></div><br></div>