Using reflexivity in Coq
<p>I was trying out the examples from the Coq documentation Software Foundations (<a href="http://www.cis.upenn.edu/~bcpierce/sf/current/Induction.html#lab40" rel="nofollow">http://www.cis.upenn.edu/~bcpierce/sf/current/Induction.html#lab40</a>) when I noticed that to solve the example give in the link:</p>

<pre><code>Theorem andb_true_elim1 : ∀b c : bool,
  andb b c = true → b = true.
Proof.
  intros b c H.
  destruct b.
  Case "b = true". (* &lt;----- here *)
    reflexivity.
  Case "b = false". (* &lt;---- and here *)
    rewrite ← H.
    reflexivity.
Qed.
</code></pre>

<p>we are destructing b which appears on the left of c for "andb". However to do the exercise that follows in the book i.e.</p>

<pre><code>Theorem andb_true_elim2 : ∀b c : bool,
  andb b c = true → c = true.
Proof.
  (* FILL IN HERE *) Admitted.
</code></pre>

<p>I found the same method does not help. "reflexivity" did not help which I assume is due to the position of 'b' in the subgoal. Eventually I completed the proof in the following manner:</p>

<pre><code>Theorem andb_true_elim2 : forall b c:bool,
andb b c = true -&gt; c = true.
Proof.
intros b c H.
destruct c.
Case "c=true".
reflexivity.
Case "c=false".
rewrite &lt;- H.
destruct b.
reflexivity.
reflexivity.
Qed.
</code></pre>

<p>Can someone explain why the above code worked and the following dint?</p>

<pre><code>Theorem andb_true_elim2 : forall b c:bool,
andb b c = true -&gt; c = true.
Proof.
intros b c H.
destruct c.
Case "c=true".
reflexivity.
Case "c=false".
rewrite &lt;- H.
reflexivity.
</code></pre>