  as the elimination rules for conjunction. The second pair of rules would often be considered to be just a more complicated variant of the pair of projections. However, from an intensional point of view, these two pairs of rules are not identical. Identifying them corresponds to identifying A ∧ B and A ∧ (A → B), which is only extensionally, but not intensionally correct. As Došen has frequently argued (e.g., Došen 1997, 2006), formulas such as A ∧ B and A ∧ (A → B) are equivalent, but not isomorphic. Here “isomorphic” means that when proving one formula from the other and vice versa, we obtain, by combining these two proofs, the identity proof. This is not the case in this example. 