proposition: Theorem snd_fst_is_swap : forall (p : natprod), (snd p, fst p) = swap_pair p.
proof: Proof. MProof. Admitted. Theorem fst_swap_is_snd : forall (p : natprod), fst (swap_pair p) = snd p. MProof. Admitted. Inductive natlist : Type := | nil : natlist | cons : nat -> natlist -> natlist. Definition mylist := cons 1 (cons 2 (cons 3 nil)). Notation "x :: l" := (cons x l) (at level 60, right associativity). Notation "[ ]" := nil. Notation "[ x ; .. ; y ]" := (cons x .. (cons y nil) ..). Definition mylist1 := 1 :: (2 :: (3 :: nil)). Definition mylist2 := 1 :: 2 :: 3 :: nil. Definition mylist3 := [1;2;3]. Fixpoint repeat (n count : nat) : natlist := match count with | O => nil | S count' => n :: (repeat n count') end. Fixpoint length (l:natlist) : nat := match l with | nil => O | h :: t => S (length t) end. Fixpoint app (l1 l2 : natlist) : natlist := match l1 with | nil => l2 | h :: t => h :: (app t l2) end. Notation "x ++ y" := (app x y) (right associativity, at level 60). Example test_app1: [1;2;3] ++ [4;5] = [1;2;3;4;5]. MProof. reflexivity. Qed.