Hi,

I struggle to prove something of the form:

```
H : (a \/ b\/ c) /\ d
============================
a /\ d
```

I thought I can use `assumption`

or `destruct`

on `H`

but without success. Is there some tactic\ ... what do I miss ?

This is not provable. However, doing `destruct H`

(and then another `destruct`

) is indeed the way to go to study the various cases.

Don't wonder why, because this doesn't hold in general.

Thank you for the fast reply guys. Rethinking this, it totally makes sense :P

for goals with simple propositional formulas (or-and-not), you can typically use the `tauto`

tactic as an oracle to check whether something is provable

While on the topic of using `tauto`

. I recall reading that `tauto`

makes use of excluded middle if the corresponding library has been imported. Does someone know whether it does something smarter than exploiting Glivenko's theorem (i.e., apply a single double negation to the top and then prove the formula constructively)?

Last updated: Sep 23 2023 at 14:01 UTC