Why are you trying to teach 16 year olds theorem proving? They're are no situations in which that will ever be interesting or useful to them, so it's no surprise they would be bored and distracted.
I teach a class on Programming Languages at a US university as part of an accredited CS program. The curriculum is what it is. I don't control who takes my class, and I don't restrict access to any student as long as they meet the prerequisites. At the beginning of the semester I get a roster, and I teach them the material.
For what it's worth, the 16 year old are usually the better behaved, as they are advanced students from high school who are beyond their peers in ability. They find the material eminently fascinating and are fully engaged. The ones to watch out for are the 21 year olds.
I personally learned Coq at 14. Who are you to decide what's interesting and useful to 16 year olds?