From Undecidability.Shared.Libs.DLW
  Require Import utils.

Set Implicit Arguments.

Set Default Proof Using "Type".

Section recursor.

  Variables (F : Prop)
            (Ffun : n m, F n F m n = m)
            (HF : ex F sig F)
            (G : Prop)
            (Gfun : x y n m, G x y n G x y m n = m)
            (HG : x y, ex (G x y) sig (G x y)).

  Fixpoint recursor n x :=
    match n with
      | 0 F x
      | S n y, recursor n y G n y x
      end.

  Fact recursor_fun n x y : recursor n x recursor n y x = y.
  Proof using Ffun Gfun.
    revert x y; induction n as [ | n IHn ]; simpl; auto.
    intros x y (a & & ) (b & & ).
    specialize (IHn _ _ ); subst b.
    revert ; apply Gfun.
  Qed.


  Fixpoint recursor_coq n (Hn : ex (recursor n)) : sig (recursor n).
  Proof using Ffun Gfun HF HG.
    destruct n as [ | n ].
    apply HF, Hn.
    refine (match recursor_coq n _ with
        | exist _ xn Hxn match @HG n xn _ with
          | exist _ xSn HxSn exist _ xSn _
        end
      end).
    * destruct Hn as (_ & y & ? & _); exists y; auto.
    * destruct Hn as (x & y & & ).
      exists x; revert ; eqgoal; do 2 f_equal.
      revert Hxn. eapply recursor_fun.
    * exists xn; auto.
  Defined.


End recursor.