fun S : store => S.(store_funcs)
     : store -> host_func
a = 
fun A : Type =>
let B := A in fun (C : Type) (u : U A C) => (A, B, C, c _ _ u)
     : forall A : Type,
       let B := A in
       forall C : Type, U A C -> Type * Type * Type * (B * A * C)

Arguments a (_ _)%type_scope _
b = 
fun A : Type => let B := A in fun (C : Type) (u : U A C) => b _ _ u
     : forall A : Type,
       let B := A in
       forall (C : Type) (u : U A C), (A, B, C, c _ _ u) = (A, B, C, c _ _ u)

Arguments b (_ _)%type_scope _