Level:
Lib
Thy
Top
:
1
Hypotheses:
f :
(1 + 1)
1
Conclusion:
i:
(1 + 1).
j:
i. f i = f j
Applied Tactic:
(InstConcl [
1
;
0
] ...')
Generated subgoals:
None
(1 + 1) 
1
i:(1 + 1). j:i. f i = f j
1
;0] ...')