match CicReduction.whd context ty with
Cic.Prod (n,s,t) ->
not (is_proof_irrelevant context s)::aux (Some (n,Cic.Decl s)::context) t
match CicReduction.whd context ty with
Cic.Prod (n,s,t) ->
not (is_proof_irrelevant context s)::aux (Some (n,Cic.Decl s)::context) t