proposition: Lemma empty_length_elements {A} (ls : t A) (H : Empty ls) : List.length (elements ls) = 0.
proof: Proof. rewrite <- M.cardinal_1. apply cardinal_Empty; assumption. Qed.
imports: Coq.FSets.FMapInterface Coq.FSets.FMapFacts Coq.Program.Program Coq.Structures.OrderedTypeEx Fiat.Common Fiat.Common.SetEq Fiat.Common.SetEqProperties Fiat.Common.List.ListFacts Fiat.Common.List.ListMorphisms Fiat.Common.LogicFacts Fiat.Common.SetoidClassInstances