Variant of the induction tactic that doesn't require using `remember` on subterms

Question

Let's say I have two relations R1 and R2. If I need to solve a problem by induction over the term R1 A (R2 B C), I need to first do remember R2 B C, otherwise I lose the information that the second argument to R1 was equal to R2 B C. Is there a variant of induction that tactic that doesn't require me to deal with this?

Answer 1

The answer is no.

The way induction works, it replaces every instance of each of the arguments with the values that appear at the same place in the inductive predicate constructors. To make this easier, the remember tactic, replaces the compound expression (R2 B C) by a variable. you can sometimes avoid this if (R2 B C) appears in your goal, but this is rare.