proposition: Lemma is_prd_spec u : is_prd_spec_ind u (is_prd i is_unit u).
proof: Proof. unfold is_prd; case u; intros; try constructor. case (eq_idx_spec); intros; subst; try constructor; auto. case_eq (is_unit p); intros; try constructor; auto. Qed.
imports: Coq(Arith NArith List) Coq(FMapPositive Relations RelationClasses) AAC_tactics(Utils Constants)