induction with hypothesis with tuple (Prod)

Stream: new members

[Z. Wu]

In the proof of t1, induction in t1 fails to induct on the hypothesis of prop R (k, v) (w, r) and I have to use a single variable for (k, v) and (w, r) to make it go through, as shown in t2. Is there a way that allows me to carry (k, v) over in the induction in t1 as if it is a single variable?

inductive prop {α: Type} (R: α → α → Prop):  α → α → Prop where
| refl : ∀(a:α), prop R a a
| trans: ∀a b c, R a b → prop R b c → prop R a c


theorem t1 {α: Type} (R: α × α -> α × α -> Prop) (k v w r: α): prop R (k, v) (w, r) -> True := by
  intro h
  induction h -- failed
  -- index in target's type is not a variable (consider using the `cases` tactic instead)
  --  (k, v)
  sorry

theorem t2 {α: Type} (R: α × α -> α × α -> Prop) (k v w r: α) kv wr: kv = (k, v) -> wr = (w, r) -> prop R kv wr -> True := by
  intro hkv hwr h -- or
  induction h -- ok
  sorry