proposition: Lemma compat_prd_unit_return x : compat_prd_unit (return_prd i is_unit x).
proof: Proof. unfold return_prd. case (is_prd_spec); intros; try constructor; auto. Qed.
imports: Coq(Arith NArith List) Coq(FMapPositive Relations RelationClasses) AAC_tactics(Utils Constants)