diff --git a/src/subsequences2.v b/src/subsequences2.v
index 8dcde1e..785ed4f 100644
--- a/src/subsequences2.v
+++ b/src/subsequences2.v
@@ -62,7 +62,7 @@ Proof.
 Qed.
 
 
-Lemma subsequence_alt_defs {X: Type} :
+Lemma Subsequence_alt_defs {X: Type} :
   forall l s : list X,
   (exists (l1: list X) (l2 : list (list X)),
     length s = length l2
@@ -109,7 +109,7 @@ Proof.
 Qed.
 
 
-Lemma subsequence_alt_defs2 {X: Type} :
+Lemma Subsequence_alt_defs2 {X: Type} :
   forall l s : list X,
   (exists (t: list bool),
     length t = length l /\ s = map snd (filter fst (combine t l)))
@@ -134,7 +134,7 @@ Proof.
 Qed.
 
 
-Theorem subsequence_flat_map {X: Type} :
+Theorem Subsequence_flat_map {X: Type} :
   forall l s : list X, Subsequence l s
   <-> exists (l1: list X) (l2 : list (list X)),
     length s = length l2
@@ -145,19 +145,19 @@ Proof.
   reflexivity. destruct H. destruct H. destruct H. apply IHs in H0.
   destruct H0. destruct H0. destruct H0. exists x. exists (x1::x2).
   split; simpl; [rewrite H0 | rewrite <- H1]; easy.
-  intro. apply subsequence_alt_defs in H. apply subsequence_alt_defs2.
+  intro. apply Subsequence_alt_defs in H. apply Subsequence_alt_defs2.
   assumption.
 Qed.
 
 
-Theorem subsequence_bools {X: Type} :
+Theorem Subsequence_bools {X: Type} :
   forall l s : list X, Subsequence l s
   <-> (exists (t: list bool),
     length t = length l /\ s = map snd (filter fst (combine t l))).
 Proof.
-  intros l s. split; intro. apply subsequence_alt_defs.
-  apply subsequence_flat_map. assumption.
-  apply subsequence_alt_defs2. assumption.
+  intros l s. split; intro. apply Subsequence_alt_defs.
+  apply Subsequence_flat_map. assumption.
+  apply Subsequence_alt_defs2. assumption.
 Qed.
 
 
@@ -172,19 +172,19 @@ Proof.
   apply IHl. destruct H0.
 
   rewrite <- Subsequence_cons_eq with (a := a) in s0.
-  apply Subsequence_cons_r in s0. rewrite subsequence_bools in s0.
-  left. rewrite subsequence_bools. assumption.
+  apply Subsequence_cons_r in s0. rewrite Subsequence_bools in s0.
+  left. rewrite Subsequence_bools. assumption.
 
   destruct s. left. apply Subsequence_nil_r.
   assert ({x=a}+{x<>a}). apply H. destruct H0. rewrite e.
   destruct IHl with (s := s); [ left | right ];
   rewrite Subsequence_cons_eq. assumption. assumption.
 
-  right. intro I. rewrite subsequence_bools in I.
+  right. intro I. rewrite Subsequence_bools in I.
   destruct I. destruct H0. destruct x0.
   symmetry in H1. apply nil_cons in H1. contradiction H1.
   destruct b. inversion H1. rewrite H3 in n0. easy.
-  apply n. rewrite subsequence_bools. exists x0; split; inversion H0; easy.
+  apply n. rewrite Subsequence_bools. exists x0; split; inversion H0; easy.
 Qed.