proposition: Lemma fold_num_sum_O: forall E T a f, @fold_num_sum E T f (num_of_nat 0) a = inl a.
proof: Proof. intros. reflexivity. Qed.
imports: ATBR(Common) ATBR(BoolView) ATBR(MyFSets MyFSetProperties MyFMapProperties) Coq(FSetPositive FMapPositive)