proposition: Lemma wo_irrefl: forall R:relation T, well_order R -> (forall x:T, ~ R x x).
proof: Proof. intuition. assert (forall y:T, Acc R y -> y <> x). intros. induction H1. intuition. rewrite H3 in H2. apply H2 with x. trivial. trivial. pose proof (wo_well_founded R H). unfold well_founded in H2. pose proof (H1 x (H2 x)). auto. Qed.
imports: Relation_Definitions Relation_Definitions_Implicit Classical_Wf Description FunctionalExtensionality Classical ZornsLemma ProofIrrelevance EnsemblesSpec