Level: Lib Thy Top:
Hypotheses:

None

Conclusion:

(x,z.x) x:Formula True Formula

Applied Tactic: ProveOpCombTyping `fnot_wf`
Generated subgoals:

None