proposition: Lemma Cr_extensional : forall (x:Ord) (f g : forall y : Ord, y < x -> (fun _ : Ord => Ensemble Ord) y), (forall (y : Ord) (p : y < x), f y p = g y p) -> ((Cr_fun f :Ensemble Ord) = (Cr_fun g :Ensemble Ord)).
proof: Proof. intros x f g H0; apply Extensionality_Ensembles; split. - unfold Cr_fun;red; unfold In;intros x0 H; case H. + auto. + right; split. * case H1; auto. * intros beta H2; decompose [and] H1. rewrite <- (H0 beta H2); auto. - unfold Cr_fun;red; unfold In;intros x0 H; case H. + auto. + right; split. * case H1;auto. * intros beta H2; decompose [and] H1; rewrite (H0 beta H2); case (H4 beta H2); auto. Qed.
imports: Coq(Arith Logic.Epsilon Ensembles Classical) ZornsLemma(CountableTypes)