proposition: Lemma carac_eq_compat : forall (A B:Type)(P:A -> Prop)(Q:B->Prop)(Pdec: dec P)(Qdec: dec Q) x y, (P x <-> Q y) -> carac Pdec x == carac Qdec y.
proof: Proof. intros; apply Ole_antisym; intuition. Qed.
imports: ALEA(Utheory) ALEA(Sets)