Level:
Lib
Thy
Top
:
Hypotheses:
None
Conclusion:
T:
.
R:T
T
. IrOrder(T;x,y.R[x;y])
Applied Tactic:
Unfold `ir_order` 0 THEN Auto
Generated subgoals:
None
T:
. R:T 
T 
. IrOrder(T;x,y.R[x;y]) 
T:. R:T T . IrOrder(T;x,y.R[x;y])