fact: Definition return_prd u := match is_prd u with | Is_nothing => right (nil (u)) | Is_op l' => right (l') | Is_unit j => left j end.
imports: Coq(Arith NArith List) Coq(FMapPositive Relations RelationClasses) AAC_tactics(Utils Constants)