How to apply Fixpoint definitions within proofs in Coq?
<p>I have some trouble understanding how to use some of the things I've defined in Coq within proofs. I have this fragment of definition and functions:</p>

<pre><code>Inductive string : Set :=
| E  : string
| s  : nat -&gt; string -&gt; string.

Inductive deduce : Set :=
|de : string -&gt; string -&gt; deduce.

Infix "|=" := de. 

Inductive Rules : deduce -&gt; Prop :=
| compress : forall (n   : nat) (A    : string), rule (( s n ( s n A))  |= ( s n A))
 | transitive : forall A B C : string, rule (A |= B) -&gt; rule (B |= C) -&gt; rule (A |= C).

Fixpoint RepString (n m : nat): string:=
match n with  
|0 =&gt; E
|S n =&gt; s m ( RepString n m)
end.
</code></pre>

<p>I need to prove something apparently easy but I bump into two problems:</p>

<pre><code>Lemma LongCompress (C : string)(n : nat): n &gt;=1 -&gt; Rules 
((RepString n 0 ) |= (s 0 E) ).
Proof.
intros.
induction n.
inversion H.
simpl.
apply compress.
</code></pre>

<p>So here I have problem one, I get: </p>

<pre><code>"Unable to unify "Rules (s ?M1805 (s ?M1805 ?M1806) |= s ?M1805 ?M1806)" with 
"Rules (s 0 (RepString n 0) |- s 0 E)".'"
</code></pre>

<p>Now, I can see why I get the error, while technically <code>RepString n 0</code> is the same as  <code>s 0 (s 0 (s 0( ... s 0 E)))</code> I simply can't find the way to let coq know that, I've tried messing with <code>apply compress with</code> like 10 different things I still can't get it right. I need to "unfold" it something like that (of course <code>unfold</code> doesn't work...). </p>

<p>I'm out of ideas and I would very much appreciate any input you have on this!</p>

<p>EDIT FROM NOW ON.</p>

<pre><code>Inductive Rules : deduce -&gt; Prop :=
| compress : forall (n   : nat) (A    : string), rule (( s n ( s n A))  |= ( s n A))
 | transitive : forall A B C : string, rule (A |= B) -&gt; rule (B |= C) -&gt; rule (A |= C)
 | inspection : forall (n m : nat) (A    : string), m &lt; n -&gt; rule ((s n A) |- (s m A)).

 Definition less (n :nat )  (A B : string) :=  B |= (s n A).
 Lemma oneLess (n m : nat):  rule (less 0 (RepString n 1) (RepString m 1)) &lt;-&gt; n&lt; m.
</code></pre>

<p>I have generalised the lemmas that Anton Trunov helped me prove, but now I bumped into another wall. I think the problem might start with the way I've written the Theorem itself, I will appreciate any ideas. </p>