pub fn conjunction_intro(pf_p: &ProofTerm, pf_q: &ProofTerm) -> ProofTerm
Construct a proof of P ∧ Q from individual proofs.