--#include "DAlgebraic2.alfa"

Ncons :: Set
  = data Z | S

DNcons :: Datoid
  = struct {
      Elem = Ncons;
      eq =
        {-#H#-}\(c1::Elem) ->
               \(c2::Elem) ->
               case c1 of {
                 (Z) ->
                   case c2 of {
                     (Z) -> true@_;
                     (S) -> false@_;};
                 (S) ->
                   case c2 of {
                     (Z) -> false@_;
                     (S) -> true@_;};};
      ref =
        {-#H#-}\(x::Elem) ->
               case x of {
                 (Z) -> tt@_;
                 (S) -> tt@_;};
      subst =
        {-#H#-}\(P::Pow Elem) ->
               \(a1::Elem) ->
               \(a2::Elem) ->
               \(h::True (eq a1 a2)) ->
               \(h'::P a1) ->
               case a1 of {
                 (Z) ->
                   case a2 of {
                     (Z) -> h';
                     (S) -> case h of { };};
                 (S) ->
                   case a2 of {
                     (Z) -> case h of { };
                     (S) -> h';};};}

sigmaN (i::Ncons) :: Sig
  = case i of {
      (Z) -> nil@_;
      (S) -> rec@_ nil@_;}

spN :: Sig
  = nonrec@_ DNcons sigmaN

ImN (X::Set) :: Set
  = Im spN X

IN :: Set
  = T spN

Izero :: IN
  = Intro@_ (si@_ Z@_ tt@_)

Isucc (n::IN) :: IN
  = Intro@_ (si@_ S@_ (Pair@_ n tt@_))

Ione :: IN
  = Isucc Izero

eqIN2 (a::IN)(b::IN) :: Bool
  = eqIt2 spN a b

eq10 :: Bool
  = eqIN2 Ione Izero

eq11 :: Bool
  = eqIN2 Ione Ione