proposition: Lemma fold_left_id : forall A (s y : list A), List.fold_left (fun acc x => acc ++x::nil) s y = y ++ s.
proof: Proof. intros A. induction s. simpl. intros. rewrite app_nil_r. reflexivity. simpl. intros. rewrite IHs. rewrite <- app_assoc. reflexivity. Qed.
imports: Coq(FSets) ATBR(Common) ATBR(BoolView)