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