Thierry's proof of the principle of infinite descent (a part) in Agda1/Alfa

gistfile1.txt

noether (A::Set)(R::rel A) :: Type
  = (P::pred A) -> ((x::A) -> ((y::A) -> R y x -> P y) -> P x) -> (x::A) -> P x
infiniteDescent (A::Set)
                (R::rel A)
                (P::pred A)
  :: noether A R -> 
     ((x::A) -> P x -> exists A (\(x1::A) -> and (R x1 x) (P x1))) -> 
     (x::A) -> not (P x)
  = \ (h1::noether A R) -> 
    \ (h2::(x::A) -> P x -> exists A (\(x1::A) -> and (R x1 x) (P x1))) -> 
    \ (x::A) -> 
    h1 (\(y::A) -> not (P y))
       (\(z::A) ->
        \(h3::(y::A) -> (x'::R y z) -> not (P y)) ->
        \(h4::P z) ->
        existsElim A (\(x1::A) -> and (R x1 z) (P x1)) N0 (h2 z h4)
         (\(y::A) ->
          \(h5::and (R y z) (P y)) ->
          h3 y (andElimLeft (R y z) (P y) h5) (andElimRight (R y z) (P y) h5)))
      x