proposition: Lemma fold_andb_true v : fold (fun _ => andb) v true <-> forall k, find k v <> Some false.
proof: Proof. FMap_convert. split; intro H; [ specialize (fun k v => H (k, v)) | ]; simpl in *; intuition eauto using diff_false_true. destruct_head prod. destruct_head bool; eauto. 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