Level: Lib Thy Top:
Hypotheses:

None

Conclusion:

(p,q,z.pq) p:Formula q:Formula True Formula

Applied Tactic: ProveOpCombTyping `fand_wf`
Generated subgoals:

None