proposition: Lemma Forall2_inv_read : forall A (IA:Inhab A) B (IB:Inhab B) P (xs:list A) (ys:list B) i, Forall2 P xs ys -> index xs i -> P xs[i] ys[i].
proof: Proof. Proof using. induction xs; introv HF Hi; rew_index in Hi; rew_list in Hi. { math. } { lets (x&xs'&M1&M2&M3) : Forall2_cons_l_inv HF. subst. do 2 rewrite read_cons_case. case_if. { auto. } { applys* IHxs. } } Qed.
imports: TLC(LibTactics LibLogic LibOperation LibReflect LibProd LibNat LibInt LibOption LibWf) TLC(LibInt)