Coherence of Subsumption, Minimum Typing and Type Checking in Fsub