Adapt to https://github.com/coq/coq/pull/19530 #1104

Annotations

10 warnings

Coq.Logic.ClassicalFacts has been replaced by

Coq.Logic.FunctionalExtensionality has been replaced by

Coq.Logic.EqdepFacts has been replaced by Stdlib.Logic.EqdepFacts.

Coq.Init.Prelude.f_equal has been replaced by

Coq.Lists.List has been replaced by Stdlib.Lists.List.

Coq.Bool.Bool has been replaced by Stdlib.Bool.Bool.

Coq.Relations.Relations has been replaced by

Coq.funind.Recdef has been replaced by Stdlib.funind.Recdef.

Coq.Wellfounded.Wellfounded has been replaced by

Automatically putting Flat_alg in Prop even though it was declared