diff --git a/formalizations/guarded-cubical/ErrorDomains.agda b/formalizations/guarded-cubical/ErrorDomains.agda
index c278d824b8b61adc10a9aab4bd045b9785af769f..a1b7ad42ebbd929cbbe1a76f134557679a773dc5 100644
--- a/formalizations/guarded-cubical/ErrorDomains.agda
+++ b/formalizations/guarded-cubical/ErrorDomains.agda
@@ -128,27 +128,21 @@ trivialize2 {X} _R_ hSym hTrans hCong hθ = fix trivialize2'
 -- (θ (next (fix θ)))  R
 -- (fix θ)
 
--- alternatively, we can drop symmetry if we assume that the relation
--- is reflexive, or at least that fix θ is related to itself.
+-- don't need symmetry
 trivialize3 : {X : Type} (_R_ : L℧ X -> L℧ X -> Type) ->
   transitive _R_ ->
   congruence _R_ ->
-  fix θ R fix θ ->
   ((x : L℧ X) -> x R (θ (next x))) ->
   ((x : L℧ X) -> x R (fix θ))
-trivialize3 {X} _R_ hTrans hCong fix-ok hθR = fix trivialize3'
+trivialize3 {X} _R_ hTrans hCong hθR = fix trivialize3'
   where
-   lem : θ (next (fix θ)) R fix θ
-   lem = subst (λ x → x R fix θ) (fix-eq θ) fix-ok
-
    trivialize3' :
     ▹ ((x : L℧ X) -> x R (fix θ)) → (x : L℧ X) -> x R (fix θ)
    trivialize3' IH lx =
-     hTrans
-       (hθR lx)
+     subst (λ y → lx R y) (sym (fix-eq θ))
        (hTrans
-         (hCong (λ t → IH t lx))
-         lem)
+         (hθR lx)
+         (hCong (λ t → IH t lx)))
 
 --------------------------------------------------------------------------