--#include "IndFam.alfa" sigmaEven (n::Nat)(b::Bool) :: OP Nat = case b of { (false) -> nonrec@_ (True (eqNat n zer@_)) (\(h::True (eqNat n zer@_)) -> nil@_); (true) -> nonrec@_ Nat (\(m::Nat) -> nonrec@_ (True (eqNat n (suc@_ (suc@_ m)))) (\(h::True (eqNat n (suc@_ (suc@_ m)))) -> rec@_ m nil@_));} opEven (n::Nat) :: OP Nat = nonrec@_ Bool (sigmaEven n) famEven :: Fam Nat = \(n::Nat) -> nonrec@_ Bool (sigmaEven n) IEven :: Nat -> Set = T Nat famEven evenZero :: IEven zer@_ = Intro@_ (si@_ false@_ (si@_ tt@_ tt@_)) evenSS (n::Nat)(en::IEven n) :: IEven (suc@_ (suc@_ n)) = Intro@_ (si@_ true@_ (si@_ n (si@_ (refENat (suc@_ (suc@_ n))) (Pair@_ en tt@_)))) evenTwo :: IEven two = evenSS zer@_ evenZero four :: Nat = suc@_ (suc@_ two) evenFour :: IEven four = evenSS two evenTwo sizeEven (j::Nat) :: T Nat famEven j -> Nat = \(h::T Nat famEven j) -> size Nat famEven j h sizeEvenTwo :: Nat = sizeEven two evenTwo sizeEvenFour :: Nat = sizeEven four evenFour {-# Alfa unfoldgoals off brief on hidetypeannots off wide typesignatures nd hiding on #-}