Function comp_id_right 

pub fn comp_id_right<F: Prop, A: Prop, B: Prop>(
    _ty_f: Ty<F, Pow<B, A>>,
) -> Eq<Comp<F, App<FId, A>>, F>

(f : a -> b) => (f . id{a} == f).