update comments

Author: m4lvin

Pdl/LocalTableau.lean

@@ -1436,7 +1436,7 @@ lemma non_eq_of_ltSequent : lt_Sequent X Y → X ≠ Y := by
   intro lt X_eq_Y
   subst X_eq_Y
   absurd lt
-  -- This us easy, because DM ordering is irreflexive.
+  -- This is easy, because the DM ordering is irreflexive.
   have := WellFounded.irrefl (instWellFoundedRelationSequent.2)
   apply this.1
 

Pdl/UnfoldBox.lean

@@ -546,7 +546,7 @@ theorem boxHelperTermination α (ℓ : TP α) :
         · simp_all [subprograms]
 
 /-- Where formulas in the unfolding can come from.
-The article also says `φ ∈ fischerLadner [⌈α⌉ψ]` which we omit here. -/
+The article also says `φ ∈ fischerLadner [⌈α⌉ψ]` which we prove later in `unfoldBox_in_FL`. -/
 theorem unfoldBoxContent α ψ :
     ∀ X ∈ (unfoldBox α ψ),
     ∀ φ ∈ X,