proposition: Lemma eq_of_extens : forall l1 l2, length l1 = length l2 -> (forall i, index l1 i -> l1[i] = l2[i]) -> l1 = l2.
proof: Proof. Proof using IA. intros. applys~ eq_of_extens_range. Qed.
imports: TLC(LibTactics LibLogic LibOperation LibReflect LibProd LibNat LibInt LibOption LibWf) TLC(LibInt)