Level:
Lib
Thy
Top
:
1
1
Hypotheses:
E :
1
1
EquivRel(
1;x,y.x E y)
x,y:
1. Dec(x E y)
Conclusion:
m:
(1 + 1). 1-1-Corresp(
m;i,j:
1//(i E j))
Applied Tactic:
(InstConcl [
1
] ...a)
Generated subgoals:
1
. 1-1-Corresp(
1;i,j:
1//(i E j))
1 
1 
1;x,y.x E y)
x,y:1. Dec(x E y)
m:(1 + 1). 1-1-Corresp(m;i,j:1//(i E j))
1
] ...a)1;i,j:1//(i E j))