```
Variables A B C P1 P2: Prop.
Lemma lem1: (A /\ B) \/ (~A /\ B) \/ (A /\~B) \/ (~A /\~B).
```

I have to demonstrate the upside mentioned predicate logic lemma and don't know how to start with intros. Can anyone give me some advice for this?

there is no point in using `intros`

when you've already declared all variables. You probably want to declare the variables and declare the proof inside a section, e.g., `Section PredicateLogic. (* code *) End PredicateLogic.`

as for how to get started, this lemma can't be proven without adding axioms from classical logic (`From Coq Require Import Classical.`

), and conjuring the premises `A \/ ~A`

and `B \/ ~B`

, e.g., via the axiom `classic`

.

Last updated: Jun 16 2024 at 01:42 UTC