proposition: Lemma fold_right_and_True_flatten ls : fold_right and True (flatten ls) <-> fold_right and True (map (fold_right and True) ls).
proof: Proof. induction ls as [|?? IHls]; try tauto; simpl. rewrite <- IHls; clear IHls. rewrite fold_right_and_True_app; reflexivity. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.ZArith.ZArith Coq.Lists.List Coq.Lists.SetoidList Coq.Bool.Bool Fiat.Common Fiat.Common.List.Operations Fiat.Common.Equality Fiat.Common.List.FlattenList Fiat.Common.LogicFacts