proposition: Lemma trueP_eq_falseP : trueP = falseP.
proof: Proof. Proof using. lets (Y&Yfix): (@prop_has_fixpoint_when_true boolP trueP). set (neg := fun b => match b with| trueP => falseP | falseP => trueP end). lets F: ((rm Yfix) neg). set (b := Y neg). asserts~ E: (b = Y neg). destruct b. { change (trueP = neg trueP) in |- *. rewrite E. rewrite~ <- F. } { change (neg falseP = falseP) in |- *. rewrite E. rewrite~ <- F. } Qed.
imports: TLC(LibTactics LibAxioms)