proposition: Lemma list_rect_ext {A P} P0 P0' Pc Pc' ls (H0 : P0 = P0') (Hc : forall a l Pl, Pc a l Pl = Pc' a l Pl) : @list_rect A P P0 Pc ls = @list_rect A P P0' Pc' ls.
proof: Proof. apply list_rect_Proper; lazy; assumption. Qed.
imports: Coq.Lists.List Coq.Setoids.Setoid Coq.Classes.Morphisms Coq.Sorting.Permutation Fiat.Common.Ensembles.EnsembleListEquivalence Fiat.Common.List.ListFacts Fiat.Common.List.Operations Fiat.Common.List.PermutationFacts Fiat.Common.List.FlattenList