proposition: Fact recursor_fun n x y : recursor n x -> recursor n y -> x = y.
proof: Proof. Proof using Ffun Gfun. revert x y; induction n as [ | n IHn ]; simpl; auto. intros x y (a & H1 & H2) (b & H3 & H4). specialize (IHn _ _ H1 H3); subst b. revert H2 H4; apply Gfun. Qed.
imports: Undecidability.Shared.Libs.DLW(utils)