+ | B.Bind (id, B.Abst u, t) ->
+ let f tt = f (B.Bind (id, B.Abst u, tt)) in
+ let f cc = type_of f g cc t in
+ let f _ = R.push f c (B.Abst u) in
+ type_of f g c u
+ | B.Bind (id, B.Void, t) ->
+ let f tt = f (B.Bind (id, B.Void, tt)) in
+ let f cc = type_of f g cc t in
+ R.push f c B.Void
+ | B.Appl (v, t) ->