Why do these theorems of propositional logic allow for the same proof in Coq?

Question

I find it mystifying why, in the following proofs, the same sequence left; right; left serves to prove each theorem, when in a proof in propositional logic (in all proof systems I know of) these two theorems would be given distinct proofs:

Theorem or_lots2 : P -> (Q \/ P \/ P) \/ Q.

Proof.
intros S.
left; right; left.
assumption.
Qed.

Theorem or_lots3 : P -> (P \/ P \/ Q) \/ Q.

Proof.
intros S.
left; right; left.
assumption.
Qed.

If anyone can explain why, or show alternative proofs which distinguish the theorems, I would be interested.

Answer 1

It is because the proof script actually proves something more general. You can see this with this script:

Theorem or_lots1 (P Q1 Q2 Q3 : Prop) : P -> (Q1 \/ P \/ Q2) \/ Q3.
Proof.
intros S.
left; right; left.
assumption.
Qed.

Theorem or_lots2 (P Q : Prop) : P -> (Q \/ P \/ P) \/ Q.
Proof.
apply or_lots1.
Qed.


Theorem or_lots3 (P Q : Prop) : P -> (P \/ P \/ Q) \/ Q.
Proof.
apply or_lots1.
Qed.