I.T38 — Linearity Census

Linearity census of TauLib: 75/80 modules fully constructive, 1 module uses Classical.em (eliminable, I.P38), 1 module uses funext tactic (CIC kernel axiom). Book I's formalization is compatible with the !-free fragment of linear logic at the object level.