proposition: Lemma G_is_functional : functional G.
proof: Proof. unfold functional. induction x; intros; inversion H; inversion H0. subst y. subst z. refl. rewrite (IHx _ _ H2 H5). refl. Qed.
imports: Coq(ClassicalChoice) CoLoR(RelUtil LogicUtil)