proposition: Theorem app_nil_r : forall (X:Type), forall l:list X, l ++ [] = l.
proof: Proof. MProof. Admitted. Theorem app_assoc : forall A (l m n:list A), l ++ m ++ n = (l ++ m) ++ n. MProof. Admitted. Lemma app_length : forall (X:Type) (l1 l2 : list X), length (l1 ++ l2) = length l1 + length l2. MProof. Admitted. Theorem rev_app_distr: forall X (l1 l2 : list X), rev (l1 ++ l2) = rev l2 ++ rev l1. MProof. Admitted. Theorem rev_involutive : forall X : Type, forall l : list X, rev (rev l) = l. MProof. Admitted. Inductive prod (X Y : Type) : Type := | pair : X -> Y -> prod X Y. Arguments pair {X} {Y} _ _. Notation "( x , y )" := (pair x y). Notation "X * Y" := (prod X Y) : type_scope. Definition fst {X Y : Type} (p : X * Y) : X := match p with | (x, y) => x end. Definition snd {X Y : Type} (p : X * Y) : Y := match p with | (x, y) => y end. Fixpoint combine {X Y : Type} (lx : list X) (ly : list Y) : list (X*Y) := match lx, ly with | [], _ => [] | _, [] => [] | x :: tx, y :: ty => (x, y) :: (combine tx ty) end. Fixpoint split {X Y : Type} (l : list (X*Y)) : (list X) * (list Y) . Admitted. Example test_split: split [(1,false);(2,false)] = ([1;2],[false;false]). MProof. Admitted. Inductive option (X:Type) : Type := | Some : X -> option X | None : option X. Arguments Some {X} _. Arguments None {X}. Fixpoint nth_error {X : Type} (l : list X) (n : nat) : option X := match l with | [] => None | a :: l' => if beq_nat n O then Some a else nth_error l' (pred n) end. Example test_nth_error1 : nth_error [4;5;6;7] 0 = Some 4. MProof. reflexivity. Qed.