proposition: Lemma classic : forall (P : Prop), P \/ ~ P.
proof: Proof. Proof using. intros. set (B1 := fun b => b = true \/ P). set (B2 := fun b => b = false \/ P). asserts H1: (ex B1). exists true. left~. asserts H2: (ex B2). exists false. left~. sets i1: (indefinite_description H1). sets i2: (indefinite_description H2). destruct (sig_proof i1) as [HA|]; [|auto]. destruct (sig_proof i2) as [HB|]; [|auto]. right. intros HP. asserts EB: (B1 = B2). apply pred_ext_1. intros b. split; intros _; right; auto. subst i1 i2. destruct EB. rewrite (proof_irrelevance H2 H1) in HB. congruence. Qed.
imports: TLC(LibTactics)