The most well-known tutorials/learning materials, including Book 1, Chapter 2 of Software Foundations for Coq and the Natural Number Game for Lean, use natural numbers to introduce induction. But there are multiple complaints by new learners that having to prove trivial facts of natural numbers via induction feels unintuitive and intimidating (one example).
Has there been any attempt at a tutorial that doesn't start with natural numbers? I can imagine using monomorphic lists instead, say a list of booleans. For example, proving associativity of list concatenation
(a ++ b) ++ c = a ++ (b ++ c) should feel less intimidating (because it is no longer a "trivial" property of natural numbers the students would have taken as granted) and more interesting than proving associativity of addition on natural numbers. And then the properties of natural numbers could be introduced by pointing to similarities with list operations.