PrintForm Definitions mb hybrid Sections GenAutomata Doc

At: tr refines and

E:Structure, P,Q_1,Q_2:((|E| List)Prop). (P refines Q_1) (P refines Q_2) (P refines (Q_1 Q_2))
By:
Unfolds [`tr_refines`;`prop_and`] 0
THEN
Reduce 0
THEN
EasyHyp
Generated subgoals:

None

About:
listfunctionpropimpliesall

PrintForm Definitions mb hybrid Sections GenAutomata Doc