diff --git a/src/EpistemicTypes/EchoBridge.agda b/src/EpistemicTypes/EchoBridge.agda
index a2b51b2..045369f 100644
--- a/src/EpistemicTypes/EchoBridge.agda
+++ b/src/EpistemicTypes/EchoBridge.agda
@@ -165,8 +165,8 @@ data _≤G_ : Grade -> Grade -> Set where
   top≤    : {g : Grade} -> g ≤G infinity
 
 ≤G-trans : {a b c : Grade} -> a ≤G b -> b ≤G c -> a ≤G c
+≤G-trans _ top≤ = top≤
 ≤G-trans (finite≤ p) (finite≤ q) = finite≤ (≤ℕ-trans p q)
-≤G-trans p top≤ = top≤
 
 ≤G-plus : (a b : Grade) -> a ≤G gradePlus a b
 ≤G-plus (finite a) (finite b) = finite≤ (≤ℕ-plus a b)
diff --git a/src/EpistemicTypes/Kripke/Residual.agda b/src/EpistemicTypes/Kripke/Residual.agda
index 22596ca..78fb4a2 100644
--- a/src/EpistemicTypes/Kripke/Residual.agda
+++ b/src/EpistemicTypes/Kripke/Residual.agda
@@ -45,8 +45,14 @@ E _ = ⊤
 -- "Thing x is here": true only at world x.
 Is : W → W → Set
 Is a a = ⊤
+Is a b = ⊥
+Is a c = ⊥
+Is b a = ⊥
 Is b b = ⊤
-Is _ _ = ⊥
+Is b c = ⊥
+Is c a = ⊥
+Is c b = ⊥
+Is c c = ⊥
 
 Present : W → Set
 Present w = Σ W (λ x → Is x w)
diff --git a/src/EpistemicTypes/ProofTransportExample.agda b/src/EpistemicTypes/ProofTransportExample.agda
index 728af25..d480aad 100644
--- a/src/EpistemicTypes/ProofTransportExample.agda
+++ b/src/EpistemicTypes/ProofTransportExample.agda
@@ -28,9 +28,9 @@ Payload _ _ = Bool
 open import EpistemicTypes.ProofTransport Agent Claim Artifact Meaning Payload
 
 checkPayload : (a : Artifact) -> (c : Claim) -> Payload a c -> Bool
+checkPayload _ ImpossibleClaim _ = false
 checkPayload true ArtifactIsTrue p = p
 checkPayload false ArtifactIsTrue _ = false
-checkPayload _ ImpossibleClaim _ = false
 
 checkPayloadSound :
   (holder : Agent) (a : Artifact) (c : Claim) (p : Payload a c) ->