proposition: Lemma read_zero : forall x l, (x::l)[0] = x.
proof: Proof. Proof using IA. intros. rewrite read_cons_case. case_if. auto. Qed.
imports: TLC(LibTactics LibLogic LibOperation LibReflect LibProd LibNat LibInt LibOption LibWf) TLC(LibInt)