proposition: Lemma exec_fst_inv r i1 r' : exec r i1 r' -> map fst r = map fst r'.
proof: Proof. induction 1 as [ | r r' x a v ev up | r r' r'' i1 i2 ex1 Ih1 ex2 Ih2 | r r' r'' b i ev ex1 Ih1 ex2 Ih2 | ]; auto. - now apply (update_index _ _ _ _ up). - now rewrite <- Ih2. - now rewrite <- Ih2. Qed.
imports: ZArith Arith List syntax little Lia