constant prop   : func(2, [@(0); @(1)])

data Peano 0 = [
  | mkZ { }
  | mkS { cS0 : Peano }
]

data Ev 0 = [
  | mkEv { cEv0 : Peano }
]

data Even 0 = [
  | mkEZ  { }
  | mkESS { cESS0 : Peano, cESS1 : Even }
]

bind 0 n : {n:Peano | true}
bind 1 p : {p:Even  | prop p = mkEv (mkS (mkS n)) && prop p = mkEv mkZ}
bind 2 m : {m:Peano | true}
bind 3 q : {q:Even  | prop q = mkEv m }
bind 4 p : {p:Even  | prop p = mkEv (mkS (mkS n)) && prop p = mkEv (mkS (mkS m))}

constraint:
  env [0; 1]
  lhs {v:Even | true}
  rhs {v:Even | prop v = mkEv n}
  id 1 tag []

constraint:
  env [0; 2; 3; 4]
  lhs {v:Even | true }
  rhs {v:Even | prop v = mkEv n}
  id 2 tag []