Somes experiments around the generation of type invariants implication.