proposition: Lemma is_sum_spec u : is_sum_spec_ind u (is_sum i is_unit u).
proof: Proof. unfold is_sum; case u; intros; try constructor. case_eq (eq_idx_bool p i); intros; subst; try constructor; auto. revert H. case eq_idx_spec; try discriminate. auto. case_eq (is_unit p); intros; try constructor. auto. Qed.
imports: Coq(Arith NArith List) Coq(FMapPositive Relations RelationClasses) AAC_tactics(Utils Constants)