title: Proving lemma with implication based on functions
body: <p>I want to prove the lemma below. I am trying to to use tactic 'destruct', but I 
          can't prove it. Please any body guide me how can I prove such lemmas. I can prove it for EmptyString, but not for variables s1 and s2. Thanks</p>
  
  <pre><code>Inductive nat : Set :=
    | O : nat
    | S : nat -&gt; nat.
  
    Inductive string : Set :=
    | EmptyString : string
    | String : ascii -&gt; string -&gt; string.
  
    Fixpoint CompStrings (sa : string) (sb : string) {struct sb}: bool :=
    match sa with
    | EmptyString =&gt; match sb with
                    | EmptyString =&gt; true
                    | String b sb'=&gt; false
                    end
    | String a sa' =&gt; match sb with
                     | EmptyString =&gt; false
                     | String b sb'=&gt; CompStrings sa' sb'
                     end
   end.
  
   Lemma Eq_lenght : forall (s1 s2 : string), 
                   (CompStrings s1 s2) = true -&gt; (Eq_nat (length s1) (length s2)) = true.
  </code></pre>