I have the current problem when using induction with Coq:I have states ST, which are pairs (A,B), where A are Addresses (nat) and B are Memories (A parameter)Open Scope type_scope.Definition Address := nat.Parameter Memory : Set.Definition State := ( Address *  Memory ).and a reflexive and transitive relation between states:    ST ==> ST',which builds on a relation that performs the 'single step' between states:    ST --> ST'Reserved Notation S '-->' S' (at level 50, left associativity).Inductive eval : State -> State -> Prop :=| eval_step : forall (a a' : nat) (m m' : Memory),  a' > a ->  (a, m) --> (a', m')where S '-->' S' := (eval S S') : type_scope.Reserved Notation S '==>' S' (at level 50, left associativity).Inductive eval_trans : State -> State -> Prop :=| refl : forall (t : State),  t ==> t| trans : forall (t t' ti : State),  t --> ti ->  ti ==> t'->  t ==> t'where S '==>' S' := (eval_trans S S') : type_scope.When performing induction on an hypothesis of the form     ST ==> ST',I should get two cases to prove.When I introduce the various parts of a state among the hypotheses and then induce over a ST==>ST' hypothesis,CoQ forgets the biding between a state and its component.E.g. if ST is A,B and I have A,B among the hypotheses, induction here will forget the binding between ST and A,B.This is a known problem (https://stackoverflow.com/questions/4519692/keeping-information-when-using-induction), that can be circumvented with a remember A,B as ST. However, in the transitive case, the remember does some wrong things, as the single step becomes    ST --> ST'    ST' ==> ST''(and an inductive hypothesis of the form, if ST' = A,B , having already ST = A,B, then ST ==> ST')The single step is performed between the same state, which should not be the case.If I drop the remember, the transitive case works fine, as expected,    ST --> ST'    ST' ==> ST''but, alas, the state ST is a generic state and not A,B.Lemma some_lemma :  forall (a a' : Address) (m m' : Memory),    (a, m) ==> (a', m') ->    (a, m) ==> (S a', m').Proof.intros a a' m m' H.induction H. (*base case*) admit.(*inductive case*) admit.(*in both cases I lost that t = (a,m), but the IH is right*)Admitted.Lemma some_lemma_v2 :  forall (a a' : Address) (m m' : Memory),    (a, m) ==> (a', m') ->    (a, m) ==> (S a', m').Proof.intros a a' m m' H.remember (a,m) as t.induction H. (*base case*) admit.(*inductive case*) (* I have that t = (a,m) and the IH sais that if ti =(a,m) then have some ==>,but ti is the state t reaches after 1 step (H)*)Admitted.Any help is greatly appreciated.I have created this example by shortening the case I am working on, I believe all the important details to be present.thank you, and sorry in case I have missed some answer being out there in the net, but I couldn't find anything useful.
Induction over a transitive relation in Coq
coq