title: Induction on predicates with product type arguments
body: <p>If I have a predicate like this:</p>
  
  <pre><code>Inductive foo : nat -&gt; nat -&gt; Prop :=
    | Foo : forall n, foo n n.
  </code></pre>
  
  <p>then I can trivially use induction to prove some dummy lemmas:</p>
  
  <pre><code>Lemma foo_refl : forall n n',
    foo n n' -&gt; n = n'.
  Proof.
    intros.
    induction H.
    reflexivity.
  Qed.
  </code></pre>
  
  <p>However, for a predicate with product type arguments:</p>
  
  <pre><code>Inductive bar : (nat * nat) -&gt; (nat * nat) -&gt; Prop :=
    | Bar : forall n m, bar (n, m) (n, m).
  </code></pre>
  
  <p>a similar proof for nearly identical lemma gets stuck because all assumptions about variables disappear:</p>
  
  <pre><code>Lemma bar_refl : forall n n' m m',
    bar (n, m) (n', m') -&gt; n = n'.
  Proof.
    intros.
    induction H.
    (* :( *)
  </code></pre>
  
  <p>Why is this happening? If I replace <code>induction</code> with <code>inversion</code>, then it behaves as expected.</p>
  
  <p>The lemma is still provable with <code>induction</code> but requires some workarounds:</p>
  
  <pre><code>Lemma bar_refl : forall n n' m m',
    bar (n, m) (n', m') -&gt; n = n'.
  Proof.
    intros.
    remember (n, m) as nm.
    remember (n', m') as n'm'.
    induction H.
    inversion Heqnm. inversion Heqn'm'. repeat subst.
    reflexivity.
  Qed.
  </code></pre>
  
  <p>Unfortunately, this way proofs gets completely cluttered and are impossible to follow for more complicated predicates.</p>
  
  <p>One obvious solution would be to declare <code>bar</code> like this:</p>
  
  <pre><code>Inductive bar' : nat -&gt; nat -&gt; nat -&gt; nat -&gt; Prop :=
    | Bar' : forall n m, bar' n m n m.
  </code></pre>
  
  <p>This solves all the problems. Yet, for my purposes, I find the previous ("tupled") approach somewhat more elegant. Is there a way to keep the predicate as it is and still be able to do manageable inductive proofs? Where does the problem even come from?</p>