write domain, property and inductive order

ocaml code

let rec append 11 12 = match 11 with | [] -> 12 | hi :: t1 -> hi :: append ti 12 let rec length 1 = match 1 with 1 [] -> o I h :: t -> 1 + length t let rec sum l = match l with | [] => 0 I h :: t > h + sum t let rec filter p 1 = match l with | [] -> [] I h :: t -> if p h then h :: filter p t else filter pt Problem 1 (30 points) Prove the following theorem by induction. Use the lecture notes as a style guide. Theorem 1. For any type a and any value 1 of type a list, we have append 1 [] = 1