Theorem LinearIndepOn.id_insert'

feat: add an element to a linear indep family, more general version (#31515)