Level:
Lib
Thy
Top
:
Hypotheses:
None
Conclusion:
(
x,z.
x
)
x:Var
True
Formula
Applied Tactic:
ProveOpCombTyping `fvar_wf`
Generated subgoals:
None
(
x,z.
x
) 
x:Var 
True Formula