-- | function from nat to nat defined by lambda abstractionf1 : nat -> nat -> nat = \(b: nat) -> \(c : nat) ->  b

-- | function from nat, nat -> nat defined by case analaysisf2 : nat -> nat -> nat =  split    zero -> split@(nat -> nat) with                zero -> zero                suc b' -> zero    suc a' -> split@(nat -> nat) with                zero -> a'                suc b' -> b'

-- | parametrized family of nats, defined by definition.g1 (b : nat) (c : nat) : nat = b

-- | Family of nat parameterized by `(x: nat), `(y: nat)-- | cannot split on parameters, can only split on fn.-- g2 (x : nat) (y : nat) : nat =--   split--     zero -> split@(nat -> nat) with--                 zero -> zero--                 suc b' -> zero--     suc a' -> split@(nat -> nat) with--                 zero -> a'--                 suc b' -> b'