Using his diagram-checker for E, Ben Northrop has determined that our third Pasch rules follows from the other diagrammatic rules. Details can be found in his MS thesis. There is a link to the thesis on the "Students" part of Avigad's web page.
Marcos Cramer and Richard Schüller have pointed out that our first superposition rule is not sufficient prove Euclid's Proposition 4. What we really need is a single rule combining the force of the two. In other words, take the set Pi to be {a' = d, angle a'b'c' = angle abc, ab = a'b', bc = b'c', ca = c'a', on(b',L), not between(b',d,g), same-side(c',h,L)} in the statement of the rule.
Moreover, we should have made it clear that in the superposition rule, the elements a', b', c' should be fresh variables, which is to say, they should not occur in Gamma, Delta, or Delta' (or, perhaps, better: one should restrict the conclusion to a subset Delta'' of Detla' which has this property). In other words, the rule should obey something like the "eigenvariable condition" on the elimination rule for the existential quantifier in natural deduction.
Rob Arthan has pointed out that in Section 4.5 the diagram to Proposition I.12, while not incorrect, is misleading: the point q need not lie on the line pd. (But see the discussion in Section 7.3 regarding misleading diagrams!)