| Con.Aux(uri)::Con.Aux(notype)::Con.Term(ty)::Con.Term(te)::patterns -> C.MutCase
(UriManager.uri_of_string uri,
int_of_string notype, deannotate ty, deannotate te,
List.map
(function
(Con.ArgProof p) -> proof2cic [] p
| Con.Aux(uri)::Con.Aux(notype)::Con.Term(ty)::Con.Term(te)::patterns -> C.MutCase
(UriManager.uri_of_string uri,
int_of_string notype, deannotate ty, deannotate te,
List.map
(function
(Con.ArgProof p) -> proof2cic [] p