is mentioned by

Thm* E:Structure, P,Q_1,Q_2:((|E| List)Prop). (P refines Q_1) (P refines Q_2) (P refines (Q_1 Q_2))

[tr_refines_and]

Try larger context: GenAutomata