(3steps) PrintForm Definitions formula Sections ClassicalProps(jlc) Doc

At: f or wf 1
1. p: Formula
2. q: Formula

pq Formula
By: Unfold `f_or` 0
Generated subgoal:

1 inr(inr(inr(inl( < p,q > )))) Formula

About:
pairinlinrmember

(3steps) PrintForm Definitions formula Sections ClassicalProps(jlc) Doc