let ctx' = (Some (name,C.Decl so))::ctx in
C.Lambda (name, merge_coercions ctx so, merge_coercions ctx' dest)
| C.LetIn (name,so,dest) ->
let ctx' = (Some (name,C.Decl so))::ctx in
C.Lambda (name, merge_coercions ctx so, merge_coercions ctx' dest)
| C.LetIn (name,so,dest) ->