proposition: Lemma rel_list_fold_left : forall l g x y, rel (fold_left F l g) x y <-> (rel g x y \/ exists a, List.In a l /\ rel (F empty a) x y).
proof: Proof. induction l; simpl. fo. intros g x y. rewrite IHl. split_all. apply hF in H. destruct H. right. exists a. tauto. tauto. right. exists x0. tauto. left. apply hF. right. hyp. subst x0. left. apply hF. left. hyp. right. exists x0. tauto. Qed.
imports: Coq(OrderedType) CoLoR(ListUtil FSetUtil FMapUtil RelUtil LogicUtil)