proposition: Lemma eq_of_extens_range : forall l1 l2, length l1 = length l2 -> (forall i, 0 <= i < length l1 -> l1[i] = l2[i]) -> l1 = l2.
proof: Proof. Proof using IA. introv HL HR. do 2 rewrite length_eq in HL. unfold read, read_inst, read_impl in HR. applys~ LibList.eq_of_extens l1 l2. { intros n L. forwards M: (rm HR) (nat_to_Z n). math. case_if. false; math. rewrite~ abs_nat in M. } Qed.
imports: TLC(LibTactics LibLogic LibOperation LibReflect LibProd LibNat LibInt LibOption LibWf) TLC(LibInt)