Let A, B and C be given.

Assume H1: finer_than B A.

Assume H2: finer_than C B.

An exact proof term for the current goal is (Subq_tra A B C H1 H2).

∎