data Zro : Set where
data One : Set where
O1 : One
data Two : Set where
O2 : Two
I2 : Two
-- w types
rec2 : (x y : Set) -> Two -> Set
rec2 x _ O2 = x
rec2 _ y I2 = y
data W (A : Set) (B : A -> Set) : Set where -- well founded trees
w : (s : A) -> B s -> W A B
sup : (a : A) -> ((B a) -> ((x : A) -> W A B )) -> W A B
natw : Set
natw = W Two (rec2 Zro One) -- nat type as w type
zero_w : natw
zero_w = sup O2 (λ x y → {!!})