I agree that sensible theorem statements can be understood, and I don’t know why you picked one that you can’t, but since you’re still curious, here’s a longer answer.

- High-school students do proofs without understanding all the time. They can solve my stupid exercise (on
` a * s * d ...`

) by algebraic computation, without understanding what the question is about. They just apply some mechanical process that you could teach computers — in fact, that is implemented in Computer Algebra Systems, IIUC. You can check the steps
- This problem can be solved by a different mechanical process (in fact, two), a bit similarly to exercises in formal logic — which can be studied by mathematicians working on (constructive) proof theory, and which are implemented in Coq. Then you can look into the solution they produce — that’s the cheating part. Most proofs
*cannot* be produced mechanically, but this one can — moreover, since this statement only uses implication (it is a statement in propositional logic), we know that if it is provable in Coq, it can be proved by such a process — the `tauto`

tactic. I added a proof script below, with some comments, but I don’t expect this to fully make sense until you work for a while through Software Foundations.

```
Lemma yourThm : forall A B, ((((A -> B) -> A) -> A) -> B) -> B.
Proof.
tauto. (* Solve the goal automatically *)
Show Proof. (* Show the proof from [tauto] as a proof term, which you might
not be familiar with *)
Restart. (* Start over, even if we are basically done and could write [Qed.] here.*)
auto. (* Solve the goal automatically with a completely different procedure. *)
Show Proof. (* Show the proof from [auto] as a proof term, which you might not be familiar with. *)
Restart.
info_auto. (* Use auto, and show the proof in a more familiar format. *)
Show Proof. (* same proof as above *)
Restart.
(* A manual proof, extracted from what [auto] does. *)
intros A B HimplImpliesB.
apply HimplImpliesB. intros HaImpliesBImpliesA.
apply HaImpliesBImpliesA. intros HA.
apply HimplImpliesB. intros _.
exact HA.
Qed.
```

After you understand enough about Coq, you can follow the proof. I can even tell you the basic idea — if you need to prove `bar`

, and you know that hypothesis `H`

tells you that `foo -> bar`

(`foo`

implies `bar`

), then you can try the `apply H`

tactic to turn your goal from `bar`

into `foo`

— this is called a backward proof step, in which you work on the conclusion `bar`

, and show that, since `foo`

implies `bar`

, to prove the goal `bar`

it’s sufficient to prove the goal `foo`

. Here, whatever `foo`

and `bar`

is, the `apply H`

proof step is certainly a plausible thing to try; usually you need more original steps, but here you don’t.