One way to prove it would be
Print classic.
Print R.
Print x.
Check R x.
Check classic (R x).
Check fun y => classic (R y).
Definition tes2 : forall x, (R x \/ ~ R x) := fun y => classic (R y).
Or using tactics
Lemma tes3 : forall x, (R x \/ ~ R x). Proof. intro. apply classic. Qed.
Print tes3.
The proof tauto
found was
Lemma tes : forall x, (R x \/ ~R x).
Proof.
intro.
eapply NNPP.
intro.
assert (R x0 -> False).
intro.
eapply H.
eapply or_introl.
exact H0.
assert (~ R x0 -> False).
intro.
eapply H.
eapply or_intror.
exact H1.
assert False.
eapply H1.
exact H0.
eapply False_ind.
exact H2.
Qed.
The intro
tactic builds lambda abstractions, and performs implication introduction and universal quantification introduction, the apply
tactic combines previously proven theorems, and performs modus ponens where the first antecedent has already been proven, the exact
tactic gives the exact proof term, and the assert
tactic also performs modus ponens where none of the antecedents of the rule are given. To see how tactics manipulate the proof term use the Show Proof
command before and after applying a tactic.