# 28 "reload.tex" type 'a list = | Nil | Cons of 'a * 'a list # 33 "reload.tex" type ornament 'a natlist : nat => 'a list with | Z => Nil | S xs => Cons(_,xs) when xs : 'a natlist let append = lifting add : _ natlist -> _ natlist -> _ natlist with #2 <- (match m with Cons(x,_) -> x) # 50 "reload.tex" type 'a list01 = | Nil01 | Cons0 of 'a list01 | Cons1 of 'a * 'a list01 # 56 "reload.tex" type ornament 'a boollist01 : bool list => 'a list01 with | Nil => Nil01 | Cons(False,xs) => Cons0(xs) when xs : 'a boollist01 | Cons(True,xs) => Cons1(_,xs) when xs : 'a boollist01 # 63 "reload.tex" let append01 = lifting append : _ boollist01 -> _ boollist01 -> _ boollist01 with #2 <- (match m with Cons1(x,_) -> x)