proposition: Lemma compat_sum_unit_return x n : compat_sum_unit (return_sum i is_unit x n).
proof: Proof. unfold return_sum. case is_sum_spec; intros; try constructor; auto. Qed.
imports: Coq(Arith NArith List) Coq(FMapPositive Relations RelationClasses) AAC_tactics(Utils Constants)