proposition: Lemma fold_num_sum_S: forall E T a f n, @fold_num_sum E T f (S n) a = match f n a with | inl a => fold_num_sum f n a | e => e end.
proof: Proof. intros. unfold fold_num_sum. replace (peanoView (S n)) with (PeanoSucc n (peanoView n)). reflexivity. apply PeanoViewUnique. Qed.
imports: ATBR(Common) ATBR(BoolView) ATBR(MyFSets MyFSetProperties MyFMapProperties) Coq(FSetPositive FMapPositive)