proposition: Lemma classicT : forall (P : Prop), {P} + {~ P}.
proof: Proof. Proof using. intros. pose (select := fun (b:bool) => if b then P else ~P). cuts (M,HP): { b:bool | select b }. destruct M. left~. right~. apply indefinite_description. destruct (prop_inv P). exists~ true. exists~ false. Qed.
imports: TLC(LibTactics)