diff --git a/Indprop.v b/Indprop.v
new file mode 100644
index 0000000..c80c062
--- /dev/null
+++ b/Indprop.v
@@ -0,0 +1,1418 @@
+From LF Require Export Logic.
+
+Fixpoint div2 (n : nat) :=
+  match n with
+  | 0 => 0
+  | 1 => 0
+  | S (S n) => S (div2 n)
+  end.
+
+Definition f (n : nat) :=
+  if even n
+  then div2 n
+  else (3 * n) + 1.
+
+Inductive Collatz_holds_for : nat -> Prop :=
+| Chf_done : Collatz_holds_for 1
+| Chf_more (n : nat) : Collatz_holds_for (f n) -> Collatz_holds_for n.
+
+Example Collatz_holds_for_12 : Collatz_holds_for 12.
+Proof.  
+ apply Chf_more. unfold f. simpl.
+ apply Chf_more. unfold f. simpl.
+ apply Chf_more. unfold f. simpl.
+ apply Chf_more. unfold f. simpl.
+ apply Chf_more. unfold f. simpl.
+ apply Chf_more. unfold f. simpl.
+ apply Chf_more. unfold f. simpl.
+ apply Chf_more. unfold f. simpl.
+ apply Chf_more. unfold f. simpl.
+ apply Chf_done.
+Qed.
+
+Conjecture collatz: forall n, Collatz_holds_for n.
+
+Inductive le : nat -> nat -> Prop :=
+| le_n (n : nat) : le n n
+| le_S (n m : nat) (H: le n m) : le n (S m).
+
+Notation "n <= m" := (le n m) (at level 70).
+Notation "n >= m" := (le m n) (at level 70).
+
+Example le_3_5 : 3 <= 5.
+Proof.
+  apply le_S. apply le_S. apply le_n.
+Qed.
+
+Inductive clos_trans {X : Type} (R : X -> X -> Prop) : X -> X -> Prop :=
+| t_step (x y : X) :
+  R x y -> clos_trans R x y
+| t_trans (x y z : X):
+  clos_trans R x y ->
+  clos_trans R y z ->
+  clos_trans R x z.
+
+Inductive close_refl_trans {X : Type} (R : X -> X -> Prop) : X -> X -> Prop :=
+| crt_step (x y : X) :
+  R x y -> close_refl_trans R x y
+| crt_refl (x : X) : close_refl_trans R x x
+| crt_trans (x y z : X) :
+  close_refl_trans R x y ->
+  close_refl_trans R y z ->
+  close_refl_trans R x z.
+
+Inductive Perm3 {X : Type} : list X -> list X -> Prop :=
+| perm3_swap12 (a b c : X) :
+  Perm3 [a;b;c] [b;a;c]
+| perm3_swap23 (a b c : X) :
+  Perm3 [a;b;c] [a;c;b]
+| perm3_trans (l1 l2 l3 : list X) :
+  Perm3 l1 l2 -> Perm3 l2 l3 -> Perm3 l1 l3.
+
+Example Perm3_exercise1 : Perm3 [1;2;3] [1;2;3].
+Proof.
+  apply perm3_trans with (l2 := [2;1;3]).
+  - apply perm3_swap12.
+  - apply perm3_swap12.
+Qed.
+
+Example Perm3_example1 : Perm3 [1;2;3] [2;3;1].
+Proof.
+  apply perm3_trans with [2;1;3].
+  - apply perm3_swap12.
+  - apply perm3_swap23.
+Qed.
+
+Inductive ev : nat -> Prop :=
+| ev_0 : ev 0
+| ev_SS (n : nat) (H : ev n) : ev (S (S n)).
+
+Example ev_4 : ev 4.
+Proof.
+  repeat apply ev_SS.
+  apply ev_0.
+Qed.
+
+Theorem ev_plus4 : forall n, ev n -> ev (4 + n).
+Proof.
+  intros n.
+  simpl.
+  intros Hn.
+  apply ev_SS.
+  apply ev_SS.
+  apply Hn.
+Qed.
+
+Theorem ev_double : forall n,
+    ev (double n).
+Proof.
+  induction n as [ | n' IHn'].
+  - simpl. apply ev_0.
+  - simpl. apply ev_SS. apply IHn'.
+Qed.
+
+Theorem ev_inversion : forall (n : nat),
+    ev n ->
+    (n = 0) \/ (exists n', n = S (S n') /\ ev n').
+Proof.
+  intros n E.
+  destruct E as [ | n' E'] eqn:EE.
+  - left. reflexivity.
+  - right. exists n'. split.
+    + reflexivity.
+    + apply E'.
+Qed.
+
+Theorem evSS_ev : forall n, ev (S (S n)) -> ev n.
+Proof.
+  intros n H.
+  apply ev_inversion in H.
+  destruct H as [H0 | H1].
+  - discriminate.
+  - destruct H1 as [n' [Hnm Hev]].
+    injection Hnm as Heq.
+    rewrite Heq. apply Hev.
+Qed.
+
+Theorem evSS_ev' : forall n,
+    ev (S (S n)) -> ev n.
+Proof.
+  intros n E.
+  inversion E as [ | n' E' Heq].
+  apply E'.
+Qed.
+
+Theorem one_not_even : ~ ev 1.
+Proof.
+  intros H.
+  inversion H.
+Qed.
+
+Theorem SSSSev_even : forall n,
+    ev (S (S (S (S n)))) -> ev n.
+Proof.
+  intros n E.
+  inversion E as [ | n' E' H].
+  inversion E' as [ | n'' E'' H1].
+  apply E''.
+Qed.
+
+Theorem SSSSev_even' : forall n,
+    ev (S (S (S (S n)))) -> ev n.
+Proof.
+  intros n E.
+  apply ev_inversion in E.
+  destruct E as [H0 | [n' [HSS E']]].
+  - discriminate.
+  - apply ev_inversion in E'.
+    destruct E' as [H0 | [n'' [HSSSS E'']]].
+    + rewrite H0 in HSS.
+      discriminate.
+    + injection HSS as HSS.
+      rewrite <- HSS in HSSSS.
+      injection HSSSS as HSSSS.
+      rewrite <- HSSSS in E''.
+      apply E''.
+Qed.
+
+Theorem ev5_nonsense :
+  ev 5 -> 2 + 2 = 9.
+Proof.
+  intros E.
+  inversion E as [ | n E' H].
+  inversion E' as [ | n' E'' H'].
+  inversion E'' as [ | n'' E''' H''].
+Qed.
+
+Example inversion_ex1 : forall (n m o : nat),
+    [n;m] = [o;o] -> [n] = [m].
+Proof.
+  intros n m o H.
+  inversion H.
+  reflexivity.
+Qed.
+
+Lemma ev_Even : forall n,
+    ev n -> Even n.
+Proof.
+  intros n E.
+  induction E as [ | n' E' IH].
+  - unfold Even. exists 0. reflexivity.
+  - unfold Even in IH.
+    destruct IH as [k Hk].
+    rewrite Hk.
+    unfold Even.
+    exists (S k).
+    reflexivity.
+Qed.
+
+Theorem ev_Even_iff : forall n,
+    ev n <-> Even n.
+Proof.
+  intros n. split.
+  - apply ev_Even.
+  - unfold Even. intros [k Hk]. rewrite Hk. apply ev_double.
+Qed.
+
+Theorem ev_sum : forall n m, ev n -> ev m -> ev (n + m).
+Proof.
+  intros n m E.
+  induction E as [ | n' E' IH].
+  - intros E.
+    simpl.
+    apply E.
+  - intros Em.
+    simpl.
+    apply ev_SS.
+    apply IH.
+    apply Em.
+Qed.
+
+Inductive ev' : nat -> Prop :=
+| ev'_0 : ev' 0
+| ev'_2 : ev' 2
+| ev'_sum n m (Hn : ev' n) (Hm : ev' m) : ev' (n + m).
+
+Theorem ev'_ev : forall n, ev' n <-> ev n.
+Proof.
+  intros n.
+  split.
+  - intros E.
+    induction E as [ | | n' m' Hn Hm].
+    + apply ev_0.
+    + apply ev_SS. apply ev_0.
+    + apply ev_sum.
+      * apply Hm.
+      * apply IHE1.
+  - intros E.
+    induction E as [ | n' E' IH].
+    + apply ev'_0.
+    + inversion E'.
+      * apply ev'_2.
+      * rewrite H0.
+        rewrite <- plus_0_n.
+        rewrite <- plus_n_Sm.
+        rewrite <- plus_n_Sm.
+        assert (G : S (0 + n') = 1 + n').
+        { reflexivity. }
+        rewrite G.
+        assert (G' : S (1 + n') = 2 + n').
+        { reflexivity. }
+        rewrite G'.
+        apply ev'_sum.
+        -- apply ev'_2.
+        -- apply IH.
+Qed.
+
+Theorem ev_ev__ev : forall n m,
+    ev (n + m) -> ev n -> ev m.
+Proof.
+  intros n m E1 E2.
+  generalize dependent E1.
+  induction E2.
+  - trivial.
+  - simpl.
+    intros H.
+    apply IHE2.
+    apply evSS_ev in H.
+    apply H.
+Qed.
+
+Theorem ev_plus_plus : forall n m p,
+    ev (n + m) -> ev (n + p) -> ev (m + p).
+Proof.
+  intros n m p E1 E2.
+  apply ev_ev__ev with (n := n + n).
+  - rewrite (add_assoc (n + n) m p).
+    rewrite add_comm.
+    rewrite (add_assoc p (n + n) m).
+    rewrite add_assoc.
+    rewrite <- (add_assoc (p + n) n m).
+    rewrite (add_comm p n).
+    apply ev_sum.
+    + apply E2.
+    + apply E1.
+  - rewrite <- double_plus.
+    apply ev_double.
+Qed.
+
+Module Playground.
+  Inductive le : nat -> nat -> Prop :=
+  | le_n (n : nat) : le n n
+  | le_S (n m : nat) (H : le n m) : le n (S m).
+
+  Notation "n <= m" := (le n m).
+
+  Example test_le1 :
+    3 <= 3.
+  Proof.
+    apply le_n. Qed.
+
+  Example test_le3 :
+    (2 <= 1) -> 2 + 2 = 5.
+  Proof.
+    intros H.
+    inversion H.
+    inversion H2.
+  Qed.
+
+  Definition lt (n m : nat) := lt (S n) m.
+  Notation "n < m" := (lt n m).
+End Playground.
+
+Inductive total_relation : nat -> nat -> Prop :=
+| rel_0 (n : nat) : total_relation 0 n
+| rel_Sn_m (n m : nat) (H : total_relation n m) : total_relation (S n) m.
+
+Theorem total_relation_is_total : forall n m, total_relation n m.
+Proof.
+  intros n m.
+  induction n as [ | n' IHn'].
+  - apply rel_0.
+  - apply rel_Sn_m.
+    apply IHn'.
+Qed.
+
+Inductive empty_relation : nat -> nat -> Prop :=
+| rel_contra (n m : nat) (H : S n = 0) : empty_relation n m.
+
+Theorem empty_relation_is_empty : forall n m, ~empty_relation n m.
+Proof.
+  intros n m contra.
+  inversion contra.
+  discriminate H.
+Qed.
+
+Lemma le_trans : forall m n o, m <= n -> n <= o -> m <= o.
+Proof.
+  intros m n o H1 H2.
+  induction H2.
+  - apply H1.
+  - apply le_S.
+    apply IHle.
+    apply H1.
+Qed.
+
+Theorem O_le_n : forall n,
+    0 <= n.
+Proof.
+  induction n as [ | n' IHn'].
+  - apply le_n.
+  - apply le_S. apply IHn'.
+Qed.
+
+Theorem n_le_m__Sn_le_Sm : forall n m,
+    n <= m -> S n <= S m.
+Proof.
+  intros n m H.
+  induction H.
+  - apply le_n.
+  - apply le_S.
+    apply IHle.
+Qed.
+
+Theorem Sn_le_Sm__n_le_m : forall n m,
+    S n <= S m -> n <= m.
+Proof.
+  intros n m.
+  generalize dependent n.
+  induction m as [ | m' IHm'].
+  - intros n H.
+    inversion H.
+    + apply le_n.
+    + inversion H2.
+  - intros n H.
+    inversion H.
+    + apply le_n.
+    + apply IHm' in H2.
+      apply le_S.
+      apply H2.
+Qed.
+
+Theorem lt_ge_cases : forall n m,
+    n <= m \/ ~(n <= m).
+Proof.
+  induction n as [ | n' IHn'].
+  - intros m.
+    left.
+    apply O_le_n.
+  - intros [ | m].
+    + right.
+      intros contra.
+      inversion contra.
+    + destruct IHn' with (m := m) as [ H | H ].
+      * left.
+        apply n_le_m__Sn_le_Sm.
+        apply H.
+      * right.
+        intros contra.
+        apply H.
+        apply Sn_le_Sm__n_le_m.
+        apply contra.
+Qed.
+
+Theorem le_plus_l : forall a b,
+    a <= a + b.
+Proof.
+  intros a b.
+  generalize dependent a.
+  induction b as [ | b' IHb'].
+  - intros a.
+    rewrite add_0_r.
+    apply le_n.
+  - intros a.
+    rewrite <- plus_n_Sm.
+    apply le_S.
+    apply IHb'.
+Qed.
+
+Theorem plus_le : forall n1 n2 m,
+    n1 + n2 <= m ->
+    n1 <= m /\ n2 <= m.
+Proof.
+  intros n1 n2 m.
+  generalize dependent n2.
+  generalize dependent n1.
+  induction m as [ | m' IHm'].
+  - intros n1 n2 H.
+    split.
+    + inversion H.
+      apply le_plus_l.
+    + inversion H.
+      rewrite add_comm.
+      apply le_plus_l.
+  - intros n1 n2 H.
+    split.
+    + inversion H.
+      * apply le_plus_l.
+      * apply IHm' in H2 as [H2 H2'].
+        apply le_S.
+        apply H2.
+    + inversion H.
+      * rewrite add_comm.
+        apply le_plus_l.
+      * apply IHm' in H2 as [H2 H2'].
+        apply le_S.
+        apply H2'.
+Qed.
+
+Theorem add_le_cases : forall n m p q,
+    n + m <= p + q -> n <= p \/ m <= q.
+Proof.
+  induction n as [ | n' IHn'].
+  { intros m p q H. left. apply O_le_n. }
+  intros m p.
+  generalize dependent m.
+  induction p as [ | p' IHp'].
+  - intros m q H.
+    assert (G : 0 + q = q).
+    { reflexivity. }
+    rewrite G in H.
+    apply plus_le in H as [H1 H2].
+    right.
+    apply H2.
+  - intros m q H.
+    simpl in H.
+    apply Sn_le_Sm__n_le_m in H.
+    apply IHn' in H as [H | H].
+    + left.
+      apply n_le_m__Sn_le_Sm.
+      apply H.
+    + right.
+      apply H.
+Qed.
+
+Theorem plus_le_compat_l : forall n m p,
+    n <= m ->
+    p + n <= p + m.
+Proof.
+  intros n m p H.
+  induction p as [ | p' IHp'].
+  - simpl. apply H.
+  - simpl. apply n_le_m__Sn_le_Sm.
+    apply IHp'.
+Qed.
+
+Theorem plus_le_compat_r : forall n m p,
+    n <= m ->
+    n + p <= m + p.
+Proof.
+  intros n m p H.
+  induction p as [ | p' IHp'].
+  - rewrite add_0_r.
+    rewrite add_0_r.
+    apply H.
+  - repeat rewrite <- plus_n_Sm.
+    apply n_le_m__Sn_le_Sm.
+    apply IHp'.
+Qed.
+
+Theorem le_plus_trans : forall n m p,
+    n <= m ->
+    n <= m + p.
+Proof.
+  intros n m p H.
+  induction p as [ | p' IHp'].
+  - rewrite add_0_r. apply H.
+  - rewrite <- plus_n_Sm.
+    apply le_S.
+    apply IHp'.
+Qed.
+
+Theorem leb_complete : forall n m,
+    n <=? m = true -> n <= m.
+Proof.
+  induction n as [ | n' IHn'].
+  - intros m H.
+    apply O_le_n.
+  - intros [ | m].
+    + intros H.
+      simpl in H.
+      discriminate H.
+    + intros H.
+      simpl in H.
+      apply n_le_m__Sn_le_Sm.
+      apply IHn'.
+      apply H.
+Qed.
+
+Theorem leb_correct : forall n m,
+    n <= m ->
+    n <=? m = true.
+Proof.
+  intros n m.
+  generalize dependent n.
+  induction m as [ | m' IHm'].
+  - intros n H.
+    inversion H.
+    reflexivity.
+  - intros [ | n].
+    + intros H.
+      reflexivity.
+    + intros H.
+      simpl.
+      apply IHm'.
+      apply Sn_le_Sm__n_le_m.
+      apply H.
+Qed.
+
+Theorem leb_iff : forall n m,
+    n <=? m = true <-> n <= m.
+Proof.
+  intros n m.
+  split.
+  - apply leb_complete.
+  - apply leb_correct.
+Qed.
+
+Theorem leb_true_trans : forall n m o,
+    n <=? m = true -> m <=? o = true -> n <=? o = true.
+Proof.
+  intros n m o H1 H2.
+  apply leb_correct.
+  apply leb_complete in H1.
+  apply leb_complete in H2.
+  apply le_trans with (n := m).
+  - apply H1.
+  - apply H2.
+Qed.
+
+Inductive R : nat -> nat -> nat -> Prop :=
+| c1 : R 0 0 0
+| c2 m n o (H : R m n o) : R (S m) n (S o)
+| c3 m n o (H : R m n o) : R m (S n) (S o)
+| c4 m n o (H : R (S m) (S n) (S (S o))) : R m n o
+| c5 m n o (H : R m n o) : R n m o.
+
+Example r112 : R 1 1 2.
+Proof.
+  apply c2.
+  apply c3.
+  apply c1.
+Qed.
+
+Definition fR : nat -> nat -> nat := plus.
+
+Theorem R_equiv_fR : forall m n o, R m n o <-> fR m n = o.
+Proof.
+  intros m n o.
+  split.
+  - intros H.
+    induction H.
+    + reflexivity.
+    + unfold fR.
+      simpl.
+      unfold fR in IHR.
+      rewrite IHR.
+      reflexivity.
+    + unfold fR.
+      rewrite <- plus_n_Sm.
+      unfold fR in IHR.
+      rewrite IHR.
+      reflexivity.
+    + unfold fR.
+      unfold fR in IHR.
+      simpl in IHR.
+      injection IHR as IHR.
+      rewrite <- plus_n_Sm in IHR.
+      injection IHR as IHR.
+      apply IHR.
+    + unfold fR.
+      unfold fR in IHR.
+      rewrite add_comm.
+      apply IHR.
+  - intros H.
+    unfold fR in H.
+    generalize dependent n.
+    generalize dependent m.
+    induction o as [ | o' IHo'].
+    + intros m n H.
+      destruct m as [ | m'].
+      * simpl in H.
+        rewrite H.
+        apply c1.
+      * simpl in H.
+        discriminate H.
+    + intros m n H.
+      destruct m as [ | m'].
+      * simpl in H.
+        rewrite H.
+        apply c3.
+        apply IHo'.
+        reflexivity.
+      * simpl in H.
+        injection H as H.
+        apply c2.
+        apply IHo'.
+        apply H.
+Qed.
+
+Inductive subseq {X : Type} : list X -> list X -> Prop :=
+| empty_sub (l : list X) : subseq [] l
+| unequal_sub (l1 l2 : list X) (x : X) (E : subseq l1 l2) : subseq l1 (x :: l2)
+| equal_sub (l1 l2 : list X) (x : X) (E : subseq l1 l2) : subseq (x :: l1) (x :: l2).
+
+Theorem subseq_refl : forall X (l : list X),
+    subseq l l.
+Proof.
+  intros x.
+  induction l as [ | h t IHt].
+  - apply empty_sub.
+  - apply equal_sub.
+    apply IHt.
+Qed.
+
+Theorem subseq_app : forall X (l1 l2 l3 : list X),
+    subseq l1 l2 ->
+    subseq l1 (l2 ++ l3).
+Proof.
+  intros X l1 l2 l3 H.
+  induction H.
+  - apply empty_sub.
+  - simpl.
+    apply unequal_sub.
+    apply IHsubseq.
+  - simpl.
+    apply equal_sub.
+    apply IHsubseq.
+Qed.
+
+Lemma tail_subseq : forall X (l1 l2 : list X) (x : X),
+    subseq (x :: l1) l2 ->
+    subseq l1 l2.
+Proof.
+  intros X l1 l2 x H.
+  induction l2 as [ | h t].
+  - inversion H.
+  - inversion H.
+    + apply unequal_sub.
+      apply IHt.
+      apply E.
+    + apply unequal_sub.
+      apply E.
+Qed.
+
+Theorem subseq_trans : forall X (l1 l2 l3 : list X),
+    subseq l1 l2 ->
+    subseq l2 l3 ->
+    subseq l1 l3.
+Proof.
+  intros X l1 l2 l3 H1 H2.
+  generalize dependent l1.
+  induction H2.
+  - intros l1 H.
+    inversion H.
+    apply empty_sub.
+  - intros l0 H.
+    apply unequal_sub.
+    apply IHsubseq.
+    apply H.
+  - intros l0 H.
+    inversion H.
+    + apply empty_sub.
+    + apply unequal_sub. apply IHsubseq. apply E.
+    + apply equal_sub.
+      apply IHsubseq.
+      apply E.
+Qed.
+
+Inductive reg_exp (T : Type) : Type :=
+| EmptySet
+| EmptyStr
+| Char (t : T)
+| App (r1 r2 : reg_exp T)
+| Union (r1 r2 : reg_exp T)
+| Star (r : reg_exp T).
+
+Arguments EmptySet {T}.
+Arguments EmptyStr {T}.
+Arguments Char {T} _.
+Arguments App {T} _ _.
+Arguments Union {T} _ _.
+Arguments Star {T} _.
+
+Reserved Notation "s =~ re" (at level 80).
+
+Inductive exp_match {T} : list T -> reg_exp T -> Prop :=
+| MEmpty : [] =~ EmptyStr
+| MChar x : [x] =~ (Char x)
+| MApp s1 re1 s2 re2
+    (H1 : s1 =~ re1)
+    (H2 : s2 =~ re2)
+  : (s1 ++ s2) =~ (App re1 re2)
+| MUnionL s1 re1 re2
+    (H1 : s1 =~ re1)
+  : s1 =~ (Union re1 re2)
+| MUnionR s2 re1 re2
+    (H2 : s2 =~ re2)
+  : s2 =~ (Union re1 re2)
+| MStar0 re : [] =~ (Star re)
+| MStarApp s1 s2 re
+    (H1 : s1 =~ re)
+    (H2 : s2 =~ (Star re))
+  : (s1 ++ s2) =~ (Star re)
+
+where "s =~ re" := (exp_match s re).
+
+Example reg_exp_ex1 : [1] =~ Char 1.
+Proof.
+  apply MChar.
+Qed.
+
+Example reg_exp_ex2 : [1; 2] =~ App (Char 1) (Char 2).
+Proof.
+  apply (MApp [1]).
+  - apply MChar.
+  - apply MChar.
+Qed.
+
+Example reg_exp_ex3 : ~ ([1; 2] =~ Char 1).
+Proof.
+  intros H.
+  inversion H.
+Qed.
+
+Fixpoint reg_exp_of_list {T} (l : list T) :=
+  match l with
+  | [] => EmptyStr
+  | x :: l' => App (Char x) (reg_exp_of_list l')
+  end.
+
+Example reg_exp_ex4 : [1; 2; 3] =~ reg_exp_of_list [1; 2; 3].
+Proof.
+  simpl. apply (MApp [1]).
+  { apply MChar. }
+  apply (MApp [2]).
+  { apply MChar. }
+  apply (MApp [3]).
+  { apply MChar. }
+  apply MEmpty.
+Qed.
+
+Lemma MStar1 :
+  forall T s (re : reg_exp T),
+    s =~ re ->
+    s =~ Star re.
+Proof.
+  intros T s re H.
+  rewrite <- (app_nil_r _ s).
+  apply MStarApp.
+  - apply H.
+  - apply MStar0.
+Qed.
+
+Lemma empty_is_empty : forall T (s : list T),
+    ~(s =~ EmptySet).
+Proof.
+  intros T s H. inversion H.
+Qed.
+
+Lemma MUnion' : forall T (s : list T) (re1 re2 : reg_exp T),
+    s =~ re1 \/ s =~ re2 ->
+    s =~ Union re1 re2.
+Proof.
+  intros T s re1 re2 [ H | H ].
+  - apply MUnionL. apply H.
+  - apply MUnionR. apply H.
+Qed.
+
+Lemma MStar' : forall T (ss : list (list T)) (re : reg_exp T),
+    (forall s, In s ss -> s =~ re) ->
+    fold app ss [] =~ Star re.
+Proof.
+  intros T.
+  induction ss as [ | h t IHt].
+  - intros re H.
+    simpl. apply MStar0.
+  - intros re H.
+    simpl. apply MStarApp.
+    + apply H.
+      simpl. left. reflexivity.
+    + apply IHt.
+      intros s H2.
+      apply H.
+      simpl. right. apply H2.
+Qed.
+
+Fixpoint re_chars {T} (re : reg_exp T) : list T :=
+  match re with
+  | EmptySet => []
+  | EmptyStr => []
+  | Char x => [x]
+  | App re1 re2 => re_chars re1 ++ re_chars re2
+  | Union re1 re2 => re_chars re1 ++ re_chars re2
+  | Star re => re_chars re
+  end.
+
+Theorem in_re_match : forall T (s : list T) (re : reg_exp T) (x : T),
+    s =~ re ->
+    In x s ->
+    In x (re_chars re).
+Proof.
+  intros T s re x Hmatch Hin.
+  induction Hmatch
+    as [
+    | x'
+    | s1 re1 s2 re2 Hmatch1 IH1 Hmatch2 IH2
+    | s1 re1 re2 Hmatch IH | re1 s2 re2 Hmatch IH
+    | re | s1 s2 re Hmatch1 IH1 Hmatch2 IH2].
+  - simpl in Hin. destruct Hin.
+  - simpl. simpl in Hin. apply Hin.
+  - simpl.
+    rewrite In_app_iff in *.
+    destruct Hin as [Hin | Hin].
+    + left. apply (IH1 Hin).
+    + right. apply (IH2 Hin).
+  - simpl. rewrite In_app_iff.
+    left. apply (IH Hin).
+  - simpl. rewrite In_app_iff. right. apply (IH Hin).
+  - destruct Hin.
+  - simpl. rewrite In_app_iff in Hin.
+    destruct Hin as [Hin | Hin].
+    + apply (IH1 Hin).
+    + apply (IH2 Hin).
+Qed.
+
+Fixpoint re_not_empty {T : Type} (re : reg_exp T) : bool :=
+  match re with
+  | EmptySet => false
+  | EmptyStr => true
+  | Char _ => true
+  | App r1 r2 => re_not_empty r1 && re_not_empty r2
+  | Union r1 r2 => re_not_empty r1 || re_not_empty r2
+  | Star r => true
+  end.
+
+Theorem re_not_empty_correct : forall T (re : reg_exp T),
+    (exists s, s =~ re) <-> re_not_empty re = true.
+Proof.
+  intros T re.
+  split.
+  - intros [s E].
+    induction E.
+    + reflexivity.
+    + reflexivity.
+    + simpl.
+      rewrite IHE1.
+      rewrite IHE2.
+      reflexivity.
+    + simpl.
+      rewrite IHE.
+      reflexivity.
+    + simpl.
+      rewrite IHE.
+      destruct (re_not_empty re1) ; reflexivity.
+    + reflexivity.
+    + apply IHE2.
+  - intros H.
+    induction re.
+    + discriminate H.
+    + exists []. apply MEmpty.
+    + exists [t]. apply MChar.
+    + simpl in H.
+      rewrite andb_true_iff in H.
+      destruct H as [H1 H2].
+      apply IHre1 in H1 as [s1 H1].
+      apply IHre2 in H2 as [s2 H2].
+      exists (s1 ++ s2).
+      apply MApp.
+      * apply H1.
+      * apply H2.
+    + simpl in H.
+      rewrite orb_true_iff in H.
+      destruct H as [H | H].
+      * apply IHre1 in H as [s H].
+        exists s.
+        apply MUnionL.
+        apply H.
+      * apply IHre2 in H as [s H].
+        exists s.
+        apply MUnionR.
+        apply H.
+    + exists [].
+      apply MStar0.
+Qed.
+
+Lemma star_app : forall T (s1 s2 : list T) (re : reg_exp T),
+    s1 =~ Star re ->
+    s2 =~ Star re ->
+    s1 ++ s2 =~ Star re.
+Proof.
+  intros T s1 s2 re H1.
+  remember (Star re) as re'.
+  induction H1.
+  - discriminate.
+  - discriminate.
+  - discriminate.
+  - discriminate.
+  - discriminate.
+  - intros H. apply H.
+  - intros H.
+    rewrite <- app_assoc.
+    apply MStarApp.
+    + apply H1_.
+    + apply IHexp_match2.
+      * apply Heqre'.
+      * apply H.
+Qed.
+
+Lemma MStar'' : forall T (s : list T) (re : reg_exp T),
+    s =~ Star re ->
+    exists ss : list (list T),
+      s = fold app ss []
+      /\ forall s', In s' ss -> s' =~ re.
+Proof.
+  intros T s re H.
+  remember (Star re) as re'.
+  induction H
+    as [ | x' | s1 re1 s2' re2 Hmatch1 IH1 Hmatch2 IH2
+       | s1 re1 re2 Hmatch IH | re1 s2' re2 Hmatch IH
+       | re'' | s1 s2' re'' Hmatch1 IH1 Hmatch2 IH2].
+  - discriminate.
+  - discriminate.
+  - discriminate.
+  - discriminate.
+  - discriminate.
+  - exists [].
+    split.
+    { reflexivity. }
+    intros s H. simpl in H. exfalso. apply H.
+  - apply IH2 in Heqre' as H2.
+    injection Heqre' as Heqre''.
+    destruct H2 as [tail [G1 G2]].
+    exists (s1 :: tail).
+    split.
+    { simpl. rewrite G1. reflexivity. }
+    intros s' H.
+    destruct H as [H | H].
+    + rewrite <- H.
+      rewrite <- Heqre''.
+      apply Hmatch1.
+    + apply G2.
+      apply H.
+Qed.
+
+Module Pumping.
+
+  Fixpoint pumping_constant {T} (re : reg_exp T) : nat :=
+    match re with
+    | EmptySet => 1
+    | EmptyStr => 1
+    | Char _ => 2
+    | App re1 re2 =>
+        pumping_constant re1 + pumping_constant re2
+    | Union re1 re2 =>
+        pumping_constant re1 + pumping_constant re2
+    | Star r => pumping_constant r
+    end.
+
+  Lemma pumping_constant_ge_1 :
+    forall T (re : reg_exp T),
+      pumping_constant re >= 1.
+  Proof.
+    intros T.
+    induction re.
+    - simpl. apply le_n.
+    - simpl. apply le_n.
+    - simpl. apply le_S. apply le_n.
+    - simpl. apply le_plus_trans. apply IHre1.
+    - simpl. apply le_plus_trans. apply IHre1.
+    - simpl. apply IHre.
+  Qed.
+
+  Lemma pumping_constant_0_false :
+    forall T (re : reg_exp T),
+      pumping_constant re <> 0.
+  Proof.
+    intros T re H.
+    assert (Hp1 : pumping_constant re >= 1).
+    { apply pumping_constant_ge_1. }
+    rewrite H in Hp1. inversion Hp1.
+  Qed.
+
+  Fixpoint napp {T} (n : nat) (l : list T) : list T :=
+    match n with
+    | 0 => []
+    | S n' => l ++ napp n' l
+    end.
+
+  Lemma napp_plus : forall T (n m : nat) (l : list T),
+      napp (n + m) l = napp n l ++ napp m l.
+  Proof.
+    intros T n m l.
+    induction n as [ | n IHn].
+    - reflexivity.
+    - simpl. rewrite IHn, app_assoc. reflexivity.
+  Qed.
+
+  Lemma napp_star :
+    forall T m s1 s2 (re : reg_exp T),
+      s1 =~ re -> s2 =~ Star re ->
+      napp m s1 ++ s2 =~ Star re.
+  Proof.
+    intros T m s1 s2 re Hs1 Hs2.
+    induction m.
+    - simpl. apply Hs2.
+    - simpl. rewrite <- app_assoc.
+      apply MStarApp.
+      + apply Hs1.
+      + apply IHm.
+  Qed.
+
+  Lemma napp_nil_nil : forall (T: Type) m,
+      @napp T m [] = [].
+  Proof.
+    intros T.
+    induction m as [ | m IHm].
+    - reflexivity.
+    - simpl. apply IHm.
+  Qed.    
+
+  Lemma weak_pumping : forall T (re : reg_exp T) s,
+      s =~ re ->
+      pumping_constant re <= length s ->
+      exists s1 s2 s3,
+        s = s1 ++ s2 ++ s3 /\
+          s2 <> [] /\
+          forall m, s1 ++ napp m s2 ++ s3 =~ re.
+  Proof.
+    intros T re s Hmatch.
+    induction Hmatch
+      as [ | x | s1 re1 s2 re2 Hmatch1 IH1 Hmatch2 IH2
+         | s1 re1 re2 Hmatch IH | re1 s2 re2 Hmatch IH
+         | re | s1 s2 re Hmatch1 IH1 Hmatch2 IH2 ].
+    - simpl. intros contra. inversion contra.
+    - simpl.
+      intros H.
+      inversion H.
+      inversion H2.
+    - simpl. rewrite app_length.
+      intros H.
+      apply add_le_cases in H as [ H | H ].
+      + apply IH1 in H as [t1 [t2 [t3 [G1 [G2 G3]]]]].
+        exists t1, t2, (t3 ++ s2).
+        split.
+        { rewrite G1. repeat rewrite app_assoc. reflexivity. }
+        split.
+        { apply G2. }
+        intros m.
+        rewrite app_assoc.
+        rewrite app_assoc.
+        apply MApp.
+        * rewrite <- app_assoc.
+          apply G3.
+        * apply Hmatch2.
+      + apply IH2 in H as [t1 [t2 [t3 [G1 [G2 G3]]]]].
+        exists (s1 ++ t1), t2, t3.
+        split.
+        { rewrite G1. repeat rewrite app_assoc. reflexivity. }
+        split.
+        { apply G2. }
+        intros m.
+        rewrite <- app_assoc.
+        apply MApp.
+        { apply Hmatch1. }
+        apply G3.
+    - simpl.
+      intros H.
+      apply plus_le in H as [H1 H2].
+      apply IH in H1 as [t1 [t2 [t3 [G1 [G2 G3]]]]].
+      exists t1, t2, t3.
+      split.
+      { apply G1. }
+      split.
+      { apply G2. }
+      intros m.
+      apply MUnionL.
+      apply G3.
+    - simpl.
+      intros H.
+      apply plus_le in H as [H1 H2].
+      apply IH in H2 as [t1 [t2 [t3 [G1 [G2 G3]]]]].
+      exists t1, t2, t3.
+      split.
+      { apply G1. }
+      split.
+      { apply G2. }
+      intros m.
+      apply MUnionR.
+      apply G3.
+    - simpl. intros H.
+      inversion H.
+      exfalso. apply pumping_constant_0_false in H2.
+      apply H2.
+    - simpl. rewrite app_length.
+      intros H.
+      simpl in IH2.
+      destruct (length s1) as [ | n] eqn:Eqls2.
+      + simpl in H.
+        apply IH2 in H as [t1 [t2 [t3 [G1 [G2 G3]]]]].
+        exists (s1 ++ t1), t2, t3.
+        split.
+        { rewrite G1. repeat rewrite <- app_assoc. reflexivity. }
+        split.
+        { apply G2. }
+        intros m.
+        rewrite <- app_assoc.
+        apply MStarApp.
+        * apply Hmatch1.          
+        * apply G3.
+      + exists [], s1, s2.
+        split.
+        { simpl. reflexivity. }
+        split.
+        * intros contra.
+          rewrite contra in Eqls2.
+          simpl in Eqls2.
+          discriminate.
+        * intros m.
+          simpl.
+          apply napp_star.
+          { apply Hmatch1. }
+          { apply Hmatch2. }
+  Qed.
+
+End Pumping.
+
+Theorem filter_not_empty_In : forall n l,
+    filter (fun x => n =? x) l <> [] ->
+    In n l.
+Proof.
+  intros n l.
+  induction l as [ | h t IHt].
+  - simpl. intros contra. apply contra. reflexivity.
+  - simpl. destruct (n =? h) eqn:H.
+    + intros _. rewrite eqb_eq in H. rewrite H. left. reflexivity.
+    + intros H'. right. apply IHt. apply H'.
+Qed.
+
+Inductive reflect (P : Prop) : bool -> Prop :=
+| ReflectT (H: P) : reflect P true
+| ReflectF (H: ~P) : reflect P false.
+
+Theorem iff_reflect : forall P b, (P <-> b = true) -> reflect P b.
+Proof.
+  intros P b H.
+  destruct b eqn:Eb.
+  + apply ReflectT. rewrite H. reflexivity.
+  + apply ReflectF. rewrite H. discriminate.
+Qed.
+
+Theorem reflect_iff : forall P b, reflect P b -> (P <-> b = true).
+Proof.
+  intros P b H.
+  inversion H as [HP Hb | HNP Hb].
+  - split.
+    + intros _.
+      reflexivity.
+    + intros _.
+      apply HP.
+  - split.
+    + intros G.
+      exfalso.
+      apply HNP.
+      apply G.
+    + intros contra.
+      discriminate contra.
+Qed.
+
+Lemma eqbP : forall n m, reflect (n = m) (n =? m).
+Proof.
+  intros n m.
+  apply iff_reflect.
+  rewrite eqb_eq.
+  reflexivity.
+Qed.
+
+Theorem filter_not_empty_In' : forall n l,
+    filter (fun x => n =? x) l <> [] ->
+    In n l.
+Proof.
+  intros n l.
+  induction l as [ | h t IHt].
+  - simpl. intros H. apply H. reflexivity.
+  - simpl. destruct (eqbP n h) as [H | H].
+    + intros _. left. rewrite H. reflexivity.
+    + intros H'. right. apply IHt. apply H'.
+Qed.
+
+Fixpoint count n l :=
+  match l with
+  | [] => 0
+  | h :: t => (if n =? h then 1 else 0) + count n t
+  end.
+
+Theorem eqbP_practice : forall n l,
+    count n l = 0 -> ~(In n l).
+Proof.
+  intros n l Hcount.
+  induction l as [ | h t IHt].
+  - simpl. intros H. apply H.
+  - intros contra. simpl in contra.
+    simpl in Hcount.
+    destruct (eqbP n h) as [H | H].
+    + simpl in Hcount. discriminate Hcount.
+    + simpl in Hcount.
+      apply H.
+      destruct contra as [contra | contra].
+      * rewrite contra. reflexivity.
+      * exfalso. apply IHt in Hcount. apply Hcount. apply contra.
+Qed.
+
+Inductive nostutter {X : Type} : list X -> Prop :=
+| nostutter_empty : nostutter []
+| nostutter_single (x : X) : nostutter [x]
+| nostutter_diff
+    (x : X)
+    (y : X)
+    (l : list X)
+    (E1 : nostutter (y :: l))
+    (E2 : x <> y): nostutter (x :: y :: l).
+
+Example test_nostutter_1 : nostutter [3;1;4;1;5;6].
+Proof.
+  repeat constructor; apply eqb_neq; auto.
+Qed.
+
+Example test_nostutter_2 : nostutter (@nil nat).
+Proof. apply nostutter_empty.
+Qed.
+
+Example test_nostutter_3 : nostutter [5].
+Proof. apply (nostutter_single 5).
+Qed.
+
+Example test_nostutter_4 : not (nostutter [3;1;1;4]).
+Proof.
+  intro.
+  repeat match goal with
+           h : nostutter _ |- _ => inversion h; clear h; subst
+         end.
+  contradiction; auto. Qed.
+
+Inductive merge {X : Type} : list X -> list X -> list X -> Prop :=
+| merge_empty2 (l1 : list X):  merge l1 [] l1
+| merge_empty1 (l2 : list X): merge [] l2 l2
+| merge_cons1 (x : X) (l1 l2 l3: list X) (E : merge l1 l2 l3):
+    merge (x :: l1) l2 (x :: l3)
+| merge_cons2 (x : X) (l1 l2 l3: list X) (E : merge l1 l2 l3):
+    merge l1 (x :: l2) (x :: l3).
+
+Theorem merge_filter : forall (X : Set) (test : X -> bool) (l l1 l2 : list X),
+    merge l1 l2 l ->
+    All (fun n => test n = true) l1 ->
+    All (fun n => test n = false) l2 ->
+    filter test l = l1.
+Proof.
+  intros X test l l1 l2 H.
+  induction H.
+  - intros H1 H2.
+    induction l1 as [ | h t IHt].
+    + reflexivity.
+    + simpl. simpl in H1.
+      destruct H1 as [H1 H1'].
+      rewrite H1.
+      apply (f_equal (fun t => h :: t)).
+      apply IHt.
+      apply H1'.
+  - simpl. intros _ H.
+    induction l2 as [ | h t IHt].
+    + reflexivity.
+    + simpl. simpl in H.
+      destruct H as [H1 H2].
+      rewrite H1.
+      apply IHt.
+      apply H2.
+  - simpl.
+    intros [H1 H2] H3.
+    rewrite H1.
+    apply (f_equal (fun t => x :: t)).
+    apply (IHmerge H2 H3).
+  - simpl.
+    intros H1 [H2 H3].
+    rewrite H2.
+    apply (IHmerge H1 H3).
+Qed.
+
+Lemma filter_subseq : forall (X: Set) (test : X -> bool) (l : list X),
+    subseq (filter test l) l.
+Proof.
+  intros X test.
+  induction l as [ | h t IHt].
+  - simpl. apply empty_sub.
+  - simpl.
+    destruct (test h) as [ | ].
+    + apply equal_sub.
+      apply IHt.
+    + apply unequal_sub.
+      apply IHt.
+Qed.
+
+Inductive pal {X: Type}: list X -> Prop :=
+| pal_empty : pal []
+| pal_single (x: X) : pal [x]
+| pal_more (x: X) (m: list X) (E : pal m) : pal (x :: m ++ [x]).
+
+Theorem pal_app_rev : forall (X: Type) (l : list X),
+    pal (l ++ (rev l)).
+Proof.
+  intros X.
+  induction l.
+  - simpl. apply pal_empty.
+  - simpl.
+    rewrite app_assoc.
+    apply pal_more.
+    apply IHl.
+Qed.
+
+Lemma rev_app_single : forall (X : Type) (l : list X) (x : X),
+    rev (l ++ [x]) = x :: (rev l).
+Proof.
+  intros X.
+  induction l as [ | h t IHt].
+  - intros x.
+    reflexivity.
+  - intros x.
+    simpl.
+    rewrite IHt.
+    reflexivity.
+Qed.  
+
+Theorem pal_rev : forall (X: Type) (l : list X), pal l -> l = rev l.
+Proof.
+  intros X l H.
+  induction H.
+  - reflexivity.
+  - reflexivity.
+  - simpl.
+    rewrite rev_app_single.
+    rewrite <- IHpal.
+    reflexivity.
+Qed.
+
+Theorem length_ind : forall {X: Type} (P : list X -> Prop),
+    P [] ->
+    (forall (l1 : list X), (forall (l2 : list X), S (length l2) <= length l1 -> P l2) -> P l1) ->
+    forall (l : list X), P l.
+Proof.    
+  intros X P H1 H2 l.
+  assert (G: forall l', S (length l') <= length l -> P l').
+  - induction l' as [ | h' t' IHt'].
+    + intros G.
+      apply H1.
+    + intros G.
+      simpl in *.
+      apply H2.
+
+  
+      
+      
+Theorem palindrome_converse : forall {X : Type} (l: list X),
+    l = rev l -> pal l.
+Proof.
+  intros X.
+  destruct l as [ | h t].
+  - intros H. apply pal_empty.
+  - intros H.
+    simpl in H.
+