proposition: Lemma fold_right_uniquize {A B} {eq_A : BoolDecR A} {Abl : BoolDec_bl (@eq A)} {Alb : BoolDec_lb (@eq A)} (f : A -> B) ls x base : List.fold_right (fun y else_case => If beq x y Then f y Else else_case) base (uniquize beq ls) = List.fold_right (fun y else_case => If beq x y Then f y Else else_case) base ls.
proof: Proof. rewrite !fold_right_beq_in_correct'. destruct (list_bin beq x ls) eqn:Heq; destruct (list_bin beq x (uniquize beq ls)) eqn:Heq'; try reflexivity; exfalso; first [ apply (list_in_bl bl) in Heq | apply (list_in_bl bl) in Heq' ]; first [ rewrite (list_in_lb lb) in Heq by (eapply uniquize_In; eassumption) | rewrite (list_in_lb lb) in Heq' by (eapply (uniquize_In_refl _ _ _ (lb eq_refl) bl); assumption) ]; try congruence. 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