proposition: Lemma f_fold_right_bool_rect {A B T} (f : T -> B) init (ls : list A) a b : f (fold_right (fun x acc => bool_rect (fun _ => T) (a x) acc (b x)) init ls) = fold_right (fun x acc => bool_rect (fun _ => B) (f (a x)) acc (b x)) (f init) ls.
proof: Proof. revert init; induction ls; simpl; trivial; intros. edestruct b; simpl; trivial. 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